Theorem rexbii 1660

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 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	rexbid 1654	. 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 1638

This theorem is referenced by:  2rexbii 1662  rexanali 1676  r19.29r 1749  r19.42v 1756  reeanv 1770  rexcom4 1815  ceqsrex2v 1881  reu7 1925  0el 2286  uni0b 2513  iuniin 2563  iunrab 2586  iinss 2590  iunn0 2597  iunin2 2598  iundif2 2600  iunun 2603  iununi 2606  iunpwss 2608  reuxfr 2894  iunpw 2904  dffr2 2909  dfepfr 2922  epfrc 2923  sucel 3032  cnvuni 3290  dffr3 3415  dminxp 3469  imaco 3487  isarep1 3563  abrexexlem2 3844  imaiun 3849  abrexex2 3856  dfrdg2 3918  rdglem1 3922  tz7.49 3944  elrnoprabg 4108  qsid 4285  prfi 4531  pwfilem 4544  zfregcl 4567  zfreg 4568  zfreg2 4569  ac6n 4729  kmlem7 4743  kmlem13 4749  numth2 4757  zorn2lem7 4766  zorn 4769  brdom7disj 4776  brdom6disj 4777  isinfcard 4859  ssxr 5513  dfinfmr 6014  infmsup 6015  supxrre 6030  infmxrcl 6033  uzwo 6387  uzwoOLD 6388  nnwof 6391  cau3ir 6852  cbvsum 6924  clmnns 7022  climunii 7035  climres 7042  infcvglem1 7156  ivthlem6 7221  ivthlem6OLD 7230  efaddlem27 7306  tgval2t 7559  fctop 7592  blrn2 7782  lmcvgnns 7879  bcthlem33 7965  isgrp2i 8011  axgroth4 8719  grothprim 8722  hhcmpl 8990  hlimunii 9029  shne0 9286  nmcopexlem1 9866  nmcopexlem2 9867  nmcfnexlem1 9895  nmcfnexlem2 9896  cdj3lem3b 10272  ntunte 10340  subsp 10429

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-ex 978  df-rex 1642

Copyright terms: Public domain