Theorem ralbii 1664

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 999	. . 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 1658	. 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 1642

This theorem is referenced by:  2ralbii 1666  ralinexa 1680  r3al 1687  r19.26-2 1748  r19.28av 1752  r19.32v 1755  r19.35 1756  cbvral2v 1799  cbvral3v 1800  ralcom4 1819  reu8 1932  sbralie 1937  r19.12sn 2440  eqsn 2470  uni0b 2518  uni0c 2519  ssint 2544  iuniin 2568  iuneq2 2573  iunss 2586  ssiin 2594  iinun2 2604  iindif2 2606  iinuni 2610  iinpw 2612  dftr3 2679  dftr4 2680  dffr2 2914  dfwe2 2930  tfis2f 3123  rexxp 3214  ralxpf 3215  reluni 3260  rninxp 3474  dminxp 3475  cnvpo 3514  dffun8 3533  funcnv3 3550  fncnv 3553  fnopab2g 3608  fint 3641  funimass4 3754  funconstss 3799  fopab2 3814  f1fvf 3866  dfrdg2 3924  tz7.48lem 3946  tz7.49 3950  fooprval 4028  oeordi 4204  oaabs 4242  ixpeq2 4345  xpmapenlem4 4485  zfinf 4606  rankc1 4685  cp 4702  bnd2 4704  aceq1 4709  aceq2 4711  ac6s2 4738  ac6sf 4740  ac6s4 4741  ac9s 4744  kmlem7 4751  kmlem12 4756  kmlem13 4757  kmlem15 4759  zorn2lem4 4771  zorn2lem6 4773  zorn2lem7 4774  zorn 4777  brdom7disj 4784  brdom6disj 4785  unidom 4788  dfinfmr 6022  infmsup 6023  xrsupsslem 6031  xrinfmsslem 6032  infmxrcl 6041  uzwo3lem2 6173  fzshftralt 6462  cau3ir 6860  cau5 6864  cvg3 6868  csbfsum 6973  fsumrev 6975  fsumshft 6977  clm1 7023  clmnns 7030  climshft 7049  climres 7050  caucvg 7107  isumcmpi 7158  infxpidmlem8 7510  isbasis2g 7562  tgval2t 7567  tgss3t 7588  basgent 7590  cctop 7602  clsval2 7635  ntreq0 7658  sncld 7737  lmbr2 7881  iscau2 7889  lmbrnns 7894  bcthlem7 7955  grpidinvlem3 8000  axgroth4 8719  grothprim 8722  adjsymt 9699  cvbr2t 10148  chpssat 10227  chrelat2 10229  chrelat3t 10235  chrelat4 10237  mdsymlem8 10274  elghom 10318  imonclem 10619  ismonc 10620  blkssatm 10639

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

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

Copyright terms: Public domain