Theorem ralbidva 1656

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 969	. 2 |- (ph -> A.xph)
2		ralbidva.1	. 2 |- ((ph /\ x e. A) -> (ps <-> ch))
3	1, 2	ralbida 1654	1 |- (ph -> (A.x e. A ps <-> A.x e. A ch))

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

This theorem is referenced by:  disjssun 2322  ordunisssuc 3078  tfindsg2 3158  weinxp 3228  funimass3 3797  f1oweALT 3897  isfinite2 4529  kmlem2 4746  iscard 4833  axsup 5487  sup3 6007  infm3 6009  suprleub 6014  dfinfmr 6022  infmsup 6023  supxr2 6037  supxrre 6038  supxrbnd 6046  supxrbnd1 6050  supxrbnd2 6051  supxrleub 6054  zextltt 6145  primet 6150  shftf 6296  indstr 6401  fzshftralt 6462  cau2 6858  cvg1 6866  negfcncf 7212  acdcALT 7446  neips 7677  islp2 7697  cncnp 7728  cncnp2 7729  metreslem 7774  isopn4 7814  metcnplem 7838  metcnp2 7840  metcn 7841  metcnss 7850  lmbrf 7882  iscauf 7891  iscau5 7893  lmss 7904  causs 7906  metelcls 7916  metcn4 7921  cncms 7948  bcthlem33 7981  nvcni 8279  va1cnlem 8292  sm1cnilem 8294  nvcnpi4 8368  nmounbi 8384  isph 8425  phoeqi 8462  minveclem9 8497  minveclem24 8512  minveclem28 8516  h2hcau 8788  h2hlm 8789  hial2eq2t 8912  hcau2 8994  hhcms 9011  hhsscms 9089  hoeq1t 9696  hoeq2t 9697  adjsymt 9699  cnvadj 9756  hhlno 9766  leop2t 9995  leoptrit 10007  mdbr2 10161  dmdbr2 10168  mddmd 10173  cdj3lem3b 10301  cnvhmpha 10448

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

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

Copyright terms: Public domain