Theorem rexbii 2540

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 2534	. 2 ⊢ (⊤ → (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐴 𝜓))
4	3	mptru 1407	1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐴 𝜓)

Syntax hints:   ↔ wb 105  ⊤wtru 1399  ∃wrex 2512

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 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-17 1575  ax-ial 1583

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-rex 2517

This theorem is referenced by:  2rexbii  2542  r19.29r  2672  r19.42v  2691  rexcom13  2700  rexrot4  2701  3reeanv  2705  cbvrex2vw  2780  cbvrex2v  2782  rexcom4  2827  rexcom4a  2828  rexcom4b  2829  ceqsrex2v  2939  clel5  2944  reu7  3002  0el  3519  iuncom  3981  iuncom4  3982  iuniin  3985  dfiunv2  4011  iunab  4022  iunin2  4039  iundif2ss  4041  iunun  4054  iunxiun  4057  iunpwss  4067  inuni  4250  iunopab  4382  sucel  4513  iunpw  4583  xpiundi  4790  xpiundir  4791  reliin  4855  rexxpf  4883  iunxpf  4884  cnvuni  4922  dmiun  4946  dfima3  5085  rniun  5154  dminxp  5188  imaco  5249  coiun  5253  isarep1  5423  rexrn  5792  ralrn  5793  elrnrexdmb  5795  fnasrn  5834  fnasrng  5836  foima2  5902  rexima  5905  ralima  5906  abrexco  5910  imaiun  5911  fliftcnv  5946  abrexex2g  6291  abrexex2  6295  tfr1onlemaccex  6557  tfrcllemaccex  6570  tfrcldm  6572  qsid  6812  eroveu  6838  ixp0  6943  infmoti  7270  eldju  7310  ficardon  7436  genpdflem  7770  genpassl  7787  genpassu  7788  nqprm  7805  nqprrnd  7806  ltnqpr  7856  ltnqpri  7857  ltexprlemm  7863  ltexprlemopl  7864  ltexprlemopu  7866  caucvgprprlemaddq  7971  caucvgprprlem1  7972  suplocexprlemml  7979  suplocexprlemloc  7984  caucvgsrlemgt1  8058  elreal  8091  axcaucvglemres  8162  axpre-suploc  8165  dfinfre  9179  suprzclex  9621  supinfneg  9872  infsupneg  9873  ublbneg  9890  4fvwrd4  10418  infssuzex  10537  caucvgre  11602  rexanuz  11609  rexfiuz  11610  resqrexlemglsq  11643  resqrexlemsqa  11645  resqrexlemex  11646  rersqreu  11649  clim0  11906  cbvsum  11981  fsum3  12009  mertenslem2  12158  cbvprod  12180  fprodseq  12205  divalgb  12547  bezoutlemmain  12630  bezoutlemex  12633  pythagtriplem2  12900  pythagtriplem19  12916  pythagtrip  12917  pceu  12929  ennnfoneleminc  13093  ennnfonelemex  13096  ennnfonelemr  13105  imasaddfnlemg  13458  tgval2  14842  ntreq0  14923  metrest  15297  plyun0  15527  clwwlknun  16362