Theorem ralbii 1659

Description: Inference adding restricted universal quantifier to both sides of an equivalence.

Hypothesis

Ref	Expression
ralbii.1	|- (ph <-> ps)

Assertion

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

Proof of Theorem ralbii

Step	Hyp	Ref	Expression
1		pm4.2 170	. 2 |- (ph <-> ph)
2	1	hbth 998	. . 3 |- ((ph <-> ph) -> A.x(ph <-> ph))
3		ralbii.1	. . . 4 |- (ph <-> ps)
4	3	a1i 8	. . 3 |- ((ph <-> ph) -> (ph <-> ps))
5	2, 4	ralbid 1653	. 2 |- ((ph <-> ph) -> (A.x e. A ph <-> A.x e. A ps))
6	1, 5	ax-mp 7	1 |- (A.x e. A ph <-> A.x e. A ps)

Syntax hints:   <-> wb 146  A.wral 1637

This theorem is referenced by:  2ralbii 1661  ralinexa 1675  r3al 1682  r19.26-2 1743  r19.28av 1747  r19.32v 1750  r19.35 1751  cbvral2v 1794  cbvral3v 1795  ralcom4 1814  reu8 1926  sbralie 1931  r19.12sn 2434  eqsn 2465  uni0b 2513  uni0c 2514  ssint 2539  iuniin 2563  iuneq2 2568  iunss 2581  ssiin 2589  iinun2 2599  iindif2 2601  iinuni 2605  iinpw 2607  dftr3 2674  dftr4 2675  dffr2 2909  dfwe2 2925  tfis2f 3118  rexxp 3209  ralxpf 3210  reluni 3255  rninxp 3468  dminxp 3469  cnvpo 3508  dffun8 3527  funcnv3 3544  fncnv 3547  fnopab2g 3602  fint 3635  funimass4 3748  funconstss 3793  fopab2 3808  f1fvf 3860  dfrdg2 3918  tz7.48lem 3940  tz7.49 3944  fooprval 4022  oeordi 4198  oaabs 4236  ixpeq2 4339  xpmapenlem4 4479  zfinf 4598  rankc1 4677  cp 4694  bnd2 4696  aceq1 4701  aceq2 4703  ac6s2 4730  ac6sf 4732  ac6s4 4733  ac9s 4736  kmlem7 4743  kmlem12 4748  kmlem13 4749  kmlem15 4751  zorn2lem4 4763  zorn2lem6 4765  zorn2lem7 4766  zorn 4769  brdom7disj 4776  brdom6disj 4777  unidom 4780  dfinfmr 6014  infmsup 6015  xrsupsslem 6023  xrinfmsslem 6024  infmxrcl 6033  uzwo3lem2 6165  fzshftralt 6454  cau3ir 6852  cau5 6856  cvg3 6860  csbfsum 6965  fsumrev 6967  fsumshft 6969  clm1 7015  clmnns 7022  climshft 7041  climres 7042  caucvg 7099  isumcmpi 7150  infxpidmlem8 7502  isbasis2g 7554  tgval2t 7559  tgss3t 7580  basgent 7582  cctop 7594  clsval2 7627  ntreq0 7650  sncld 7726  lmbr2 7867  iscau2 7875  bcthlem7 7939  grpidinvlem3 7984  axgroth4 8719  grothprim 8722  adjsymt 9676  cvbr2t 10120  chpssat 10198  chrelat2 10200  chrelat3t 10206  chrelat4 10208  mdsymlem8 10245  elghom 10289  imonclem 10583  ismonc 10584  blkssatm 10603

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 960  ax-4 970  ax-5o 972

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

Copyright terms: Public domain