Theorem ralbidva 1659

Description: Formula-building rule for restricted universal quantifier (deduction rule).

Hypothesis

Ref	Expression
ralbidva.1	|- ((ph /\ x e. A) -> (ps <-> ch))

Assertion

Ref	Expression
ralbidva	|- (ph -> (A.x e. A ps <-> A.x e. A ch))

Distinct variable group:   ph,x

Proof of Theorem ralbidva

Step	Hyp	Ref	Expression
1		ax-17 971	. 2 |- (ph -> A.xph)
2		ralbidva.1	. 2 |- ((ph /\ x e. A) -> (ps <-> ch))
3	1, 2	ralbida 1657	1 |- (ph -> (A.x e. A ps <-> A.x e. A ch))

Syntax hints:   -> wi 3   <-> wb 146   /\ wa 223   e. wcel 958  A.wral 1645

This theorem is referenced by:  disjssun 2326  ordunisssuc 3083  tfindsg2 3163  weinxp 3233  funimass3 3806  f1oweALT 3906  isfinite2OLD 4546  kmlem2 4766  iscard 4853  axsup 5507  sup3 6052  infm3 6054  suprleub 6059  dfinfmr 6067  infmsup 6068  supxr2 6082  supxrre 6083  supxrbnd 6091  supxrbnd1 6095  supxrbnd2 6096  supxrleub 6099  zextltt 6190  primet 6195  shftf 6351  indstr 6461  fzshftralt 6522  cau2 6913  cvg1 6921  negfcncf 7269  acdcALT 7496  neips 7727  islp2 7747  cncnp 7778  cncnp2 7779  metreslem 7822  isopn4 7862  metcnplem 7886  metcnp2 7888  metcn 7889  metcnss 7898  lmbrf 7930  iscauf 7939  iscau5 7941  iscaunns 7944  lmss 7953  causs 7955  metelcls 7965  metcn4 7971  cncms 7998  bcthlem33 8031  nvcni 8329  nvcni2 8330  nvcni3 8331  va1cnlem 8345  sm1cnilem 8347  nvcnpi3 8422  nvcnpi4 8423  nmounbi 8439  isph 8481  phoeqi 8518  minveclem9 8553  minveclem24 8568  minveclem28 8572  h2hcau 8849  h2hlm 8850  hial2eq2t 8973  hcau2 9055  hhcms 9072  hhsscms 9150  projlemHIL 9218  hoeq1t 9756  hoeq2t 9757  adjsymt 9759  cnvadj 9816  hhlno 9826  leop2t 10057  leoptrit 10069  mdbr2 10223  dmdbr2 10230  mddmd 10236  cdj3lem3b 10367  cnvhmpha 10525

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 963  ax-17 971  ax-4 973  ax-5o 975

This theorem depends on definitions:  df-bi 147  df-an 225  df-ral 1649

Copyright terms: Public domain