Theorem rexbii 2537

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

Syntax hints:   ↔ wb 105  ⊤wtru 1396  ∃wrex 2509

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 1493  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-4 1556  ax-17 1572  ax-ial 1580

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-rex 2514

This theorem is referenced by:  2rexbii  2539  r19.29r  2669  r19.42v  2688  rexcom13  2697  rexrot4  2698  3reeanv  2702  cbvrex2vw  2777  cbvrex2v  2779  rexcom4  2823  rexcom4a  2824  rexcom4b  2825  ceqsrex2v  2935  clel5  2940  reu7  2998  0el  3514  iuncom  3971  iuncom4  3972  iuniin  3975  dfiunv2  4001  iunab  4012  iunin2  4029  iundif2ss  4031  iunun  4044  iunxiun  4047  iunpwss  4057  inuni  4239  iunopab  4370  sucel  4501  iunpw  4571  xpiundi  4777  xpiundir  4778  reliin  4841  rexxpf  4869  iunxpf  4870  cnvuni  4908  dmiun  4932  dfima3  5071  rniun  5139  dminxp  5173  imaco  5234  coiun  5238  isarep1  5407  rexrn  5774  ralrn  5775  elrnrexdmb  5777  fnasrn  5815  fnasrng  5817  foima2  5881  rexima  5884  ralima  5885  abrexco  5889  imaiun  5890  fliftcnv  5925  abrexex2g  6271  abrexex2  6275  tfr1onlemaccex  6500  tfrcllemaccex  6513  tfrcldm  6515  qsid  6755  eroveu  6781  ixp0  6886  infmoti  7203  eldju  7243  ficardon  7369  genpdflem  7702  genpassl  7719  genpassu  7720  nqprm  7737  nqprrnd  7738  ltnqpr  7788  ltnqpri  7789  ltexprlemm  7795  ltexprlemopl  7796  ltexprlemopu  7798  caucvgprprlemaddq  7903  caucvgprprlem1  7904  suplocexprlemml  7911  suplocexprlemloc  7916  caucvgsrlemgt1  7990  elreal  8023  axcaucvglemres  8094  axpre-suploc  8097  dfinfre  9111  suprzclex  9553  supinfneg  9798  infsupneg  9799  ublbneg  9816  4fvwrd4  10344  infssuzex  10461  caucvgre  11500  rexanuz  11507  rexfiuz  11508  resqrexlemglsq  11541  resqrexlemsqa  11543  resqrexlemex  11544  rersqreu  11547  clim0  11804  cbvsum  11879  fsum3  11906  mertenslem2  12055  cbvprod  12077  fprodseq  12102  divalgb  12444  bezoutlemmain  12527  bezoutlemex  12530  pythagtriplem2  12797  pythagtriplem19  12813  pythagtrip  12814  pceu  12826  ennnfoneleminc  12990  ennnfonelemex  12993  ennnfonelemr  13002  imasaddfnlemg  13355  tgval2  14733  ntreq0  14814  metrest  15188  plyun0  15418