Theorem rexbii 1665

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

Hypothesis

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

Assertion

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

Proof of Theorem rexbii

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	rexbid 1659	. 2 |- ((ph <-> ph) -> (E.x e. A ph <-> E.x e. A ps))
6	1, 5	ax-mp 7	1 |- (E.x e. A ph <-> E.x e. A ps)

Syntax hints:   <-> wb 146  E.wrex 1643

This theorem is referenced by:  2rexbii 1667  rexanali 1681  r19.29r 1754  r19.42v 1761  reeanv 1775  rexcom4 1820  ceqsrex2v 1886  reu7 1931  0el 2292  uni0b 2518  iuniin 2568  iunrab 2591  iinss 2595  iunn0 2602  iunin2 2603  iundif2 2605  iunun 2608  iununi 2611  iunpwss 2613  reuxfr 2899  iunpw 2909  dffr2 2914  dfepfr 2927  epfrc 2928  sucel 3037  cnvuni 3296  dffr3 3423  dminxp 3475  imaco 3493  isarep1 3569  abrexexlem2 3850  imaiun 3855  abrexex2 3862  dfrdg2 3924  rdglem1 3928  tz7.49 3950  elrnoprabg 4114  qsid 4291  prfi 4537  pwfilem 4550  zfregcl 4575  zfreg 4576  zfreg2 4577  ac6n 4737  kmlem7 4751  kmlem13 4757  numth2 4765  zorn2lem7 4774  zorn 4777  brdom7disj 4784  brdom6disj 4785  isinfcard 4867  ssxr 5521  dfinfmr 6022  infmsup 6023  supxrre 6038  infmxrcl 6041  uzwo 6395  uzwoOLD 6396  nnwof 6399  cau3ir 6860  cbvsum 6932  clmnns 7030  climunii 7043  climres 7050  infcvglem1 7164  ivthlem6 7229  ivthlem6OLD 7238  efaddlem27 7314  tgval2t 7567  fctop 7600  blrn2 7794  lmbrnns 7894  lmcvgnns 7895  bcthlem33 7981  isgrp2i 8026  axgroth4 8719  grothprim 8722  axhcompl 8807  hhcmpl 9008  hlimunii 9047  shne0 9309  nmcopexlem1 9889  nmcopexlem2 9890  nmcfnexlem1 9918  nmcfnexlem2 9919  cdj3lem3b 10301  ntunte 10376  subsp 10465

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-ex 979  df-rex 1647

Copyright terms: Public domain