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  3970  iuncom4  3971  iuniin  3974  dfiunv2  4000  iunab  4011  iunin2  4028  iundif2ss  4030  iunun  4043  iunxiun  4046  iunpwss  4056  inuni  4238  iunopab  4369  sucel  4498  iunpw  4568  xpiundi  4774  xpiundir  4775  reliin  4838  rexxpf  4866  iunxpf  4867  cnvuni  4905  dmiun  4929  dfima3  5067  rniun  5135  dminxp  5169  imaco  5230  coiun  5234  isarep1  5403  rexrn  5765  ralrn  5766  elrnrexdmb  5768  fnasrn  5806  fnasrng  5808  foima2  5868  rexima  5871  ralima  5872  abrexco  5876  imaiun  5877  fliftcnv  5912  abrexex2g  6255  abrexex2  6259  tfr1onlemaccex  6484  tfrcllemaccex  6497  tfrcldm  6499  qsid  6737  eroveu  6763  ixp0  6868  infmoti  7183  eldju  7223  ficardon  7349  genpdflem  7682  genpassl  7699  genpassu  7700  nqprm  7717  nqprrnd  7718  ltnqpr  7768  ltnqpri  7769  ltexprlemm  7775  ltexprlemopl  7776  ltexprlemopu  7778  caucvgprprlemaddq  7883  caucvgprprlem1  7884  suplocexprlemml  7891  suplocexprlemloc  7896  caucvgsrlemgt1  7970  elreal  8003  axcaucvglemres  8074  axpre-suploc  8077  dfinfre  9091  suprzclex  9533  supinfneg  9778  infsupneg  9779  ublbneg  9796  4fvwrd4  10324  infssuzex  10440  caucvgre  11478  rexanuz  11485  rexfiuz  11486  resqrexlemglsq  11519  resqrexlemsqa  11521  resqrexlemex  11522  rersqreu  11525  clim0  11782  cbvsum  11857  fsum3  11884  mertenslem2  12033  cbvprod  12055  fprodseq  12080  divalgb  12422  bezoutlemmain  12505  bezoutlemex  12508  pythagtriplem2  12775  pythagtriplem19  12791  pythagtrip  12792  pceu  12804  ennnfoneleminc  12968  ennnfonelemex  12971  ennnfonelemr  12980  imasaddfnlemg  13333  tgval2  14710  ntreq0  14791  metrest  15165  plyun0  15395