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  4240  iunopab  4371  sucel  4502  iunpw  4572  xpiundi  4779  xpiundir  4780  reliin  4844  rexxpf  4872  iunxpf  4873  cnvuni  4911  dmiun  4935  dfima3  5074  rniun  5142  dminxp  5176  imaco  5237  coiun  5241  isarep1  5410  rexrn  5777  ralrn  5778  elrnrexdmb  5780  fnasrn  5818  fnasrng  5820  foima2  5884  rexima  5887  ralima  5888  abrexco  5892  imaiun  5893  fliftcnv  5928  abrexex2g  6274  abrexex2  6278  tfr1onlemaccex  6505  tfrcllemaccex  6518  tfrcldm  6520  qsid  6760  eroveu  6786  ixp0  6891  infmoti  7211  eldju  7251  ficardon  7377  genpdflem  7710  genpassl  7727  genpassu  7728  nqprm  7745  nqprrnd  7746  ltnqpr  7796  ltnqpri  7797  ltexprlemm  7803  ltexprlemopl  7804  ltexprlemopu  7806  caucvgprprlemaddq  7911  caucvgprprlem1  7912  suplocexprlemml  7919  suplocexprlemloc  7924  caucvgsrlemgt1  7998  elreal  8031  axcaucvglemres  8102  axpre-suploc  8105  dfinfre  9119  suprzclex  9561  supinfneg  9807  infsupneg  9808  ublbneg  9825  4fvwrd4  10353  infssuzex  10470  caucvgre  11513  rexanuz  11520  rexfiuz  11521  resqrexlemglsq  11554  resqrexlemsqa  11556  resqrexlemex  11557  rersqreu  11560  clim0  11817  cbvsum  11892  fsum3  11919  mertenslem2  12068  cbvprod  12090  fprodseq  12115  divalgb  12457  bezoutlemmain  12540  bezoutlemex  12543  pythagtriplem2  12810  pythagtriplem19  12826  pythagtrip  12827  pceu  12839  ennnfoneleminc  13003  ennnfonelemex  13006  ennnfonelemr  13015  imasaddfnlemg  13368  tgval2  14746  ntreq0  14827  metrest  15201  plyun0  15431