Theorem rexbii 2514

Description: Inference adding restricted existential quantifier to both sides of an equivalence. (Contributed by NM, 23-Nov-1994.) (Revised by Mario Carneiro, 17-Oct-2016.)

Hypothesis

Ref	Expression
ralbii.1	⊢ (𝜑 ↔ 𝜓)

Assertion

Ref	Expression
rexbii	⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐴 𝜓)

Proof of Theorem rexbii

Step	Hyp	Ref	Expression
1		ralbii.1	. . . 4 ⊢ (𝜑 ↔ 𝜓)
2	1	a1i 9	. . 3 ⊢ (⊤ → (𝜑 ↔ 𝜓))
3	2	rexbidv 2508	. 2 ⊢ (⊤ → (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐴 𝜓))
4	3	mptru 1382	1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐴 𝜓)

Syntax hints:   ↔ wb 105  ⊤wtru 1374  ∃wrex 2486

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1471  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-4 1534  ax-17 1550  ax-ial 1558

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1485  df-rex 2491

This theorem is referenced by:  2rexbii  2516  r19.29r  2645  r19.42v  2664  rexcom13  2673  rexrot4  2674  3reeanv  2678  cbvrex2vw  2751  cbvrex2v  2753  rexcom4  2797  rexcom4a  2798  rexcom4b  2799  ceqsrex2v  2907  clel5  2912  reu7  2970  0el  3485  iuncom  3936  iuncom4  3937  iuniin  3940  dfiunv2  3966  iunab  3977  iunin2  3994  iundif2ss  3996  iunun  4009  iunxiun  4012  iunpwss  4022  inuni  4204  iunopab  4333  sucel  4462  iunpw  4532  xpiundi  4738  xpiundir  4739  reliin  4802  rexxpf  4830  iunxpf  4831  cnvuni  4869  dmiun  4893  dfima3  5031  rniun  5099  dminxp  5133  imaco  5194  coiun  5198  isarep1  5366  rexrn  5727  ralrn  5728  elrnrexdmb  5730  fnasrn  5768  fnasrng  5770  foima2  5830  rexima  5833  ralima  5834  abrexco  5838  imaiun  5839  fliftcnv  5874  abrexex2g  6215  abrexex2  6219  tfr1onlemaccex  6444  tfrcllemaccex  6457  tfrcldm  6459  qsid  6697  eroveu  6723  ixp0  6828  infmoti  7142  eldju  7182  ficardon  7308  genpdflem  7633  genpassl  7650  genpassu  7651  nqprm  7668  nqprrnd  7669  ltnqpr  7719  ltnqpri  7720  ltexprlemm  7726  ltexprlemopl  7727  ltexprlemopu  7729  caucvgprprlemaddq  7834  caucvgprprlem1  7835  suplocexprlemml  7842  suplocexprlemloc  7847  caucvgsrlemgt1  7921  elreal  7954  axcaucvglemres  8025  axpre-suploc  8028  dfinfre  9042  suprzclex  9484  supinfneg  9729  infsupneg  9730  ublbneg  9747  4fvwrd4  10275  infssuzex  10389  caucvgre  11342  rexanuz  11349  rexfiuz  11350  resqrexlemglsq  11383  resqrexlemsqa  11385  resqrexlemex  11386  rersqreu  11389  clim0  11646  cbvsum  11721  fsum3  11748  mertenslem2  11897  cbvprod  11919  fprodseq  11944  divalgb  12286  bezoutlemmain  12369  bezoutlemex  12372  pythagtriplem2  12639  pythagtriplem19  12655  pythagtrip  12656  pceu  12668  ennnfoneleminc  12832  ennnfonelemex  12835  ennnfonelemr  12844  imasaddfnlemg  13196  tgval2  14573  ntreq0  14654  metrest  15028  plyun0  15258