Theorem rexbii 2484

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

Syntax hints:   ↔ wb 105  ⊤wtru 1354  ∃wrex 2456

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 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510  ax-17 1526  ax-ial 1534

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1461  df-rex 2461

This theorem is referenced by:  2rexbii  2486  r19.29r  2615  r19.42v  2634  rexcom13  2642  rexrot4  2643  3reeanv  2647  cbvrex2vw  2715  cbvrex2v  2717  rexcom4  2760  rexcom4a  2761  rexcom4b  2762  ceqsrex2v  2869  clel5  2874  reu7  2932  0el  3445  iuncom  3892  iuncom4  3893  iuniin  3896  dfiunv2  3922  iunab  3933  iunin2  3950  iundif2ss  3952  iunun  3965  iunxiun  3968  iunpwss  3978  inuni  4155  iunopab  4281  sucel  4410  iunpw  4480  xpiundi  4684  xpiundir  4685  reliin  4748  rexxpf  4774  iunxpf  4775  cnvuni  4813  dmiun  4836  dfima3  4973  rniun  5039  dminxp  5073  imaco  5134  coiun  5138  isarep1  5302  rexrn  5653  ralrn  5654  elrnrexdmb  5656  fnasrn  5694  fnasrng  5696  foima2  5752  rexima  5755  ralima  5756  abrexco  5759  imaiun  5760  fliftcnv  5795  abrexex2g  6120  abrexex2  6124  tfr1onlemaccex  6348  tfrcllemaccex  6361  tfrcldm  6363  qsid  6599  eroveu  6625  ixp0  6730  infmoti  7026  eldju  7066  genpdflem  7505  genpassl  7522  genpassu  7523  nqprm  7540  nqprrnd  7541  ltnqpr  7591  ltnqpri  7592  ltexprlemm  7598  ltexprlemopl  7599  ltexprlemopu  7601  caucvgprprlemaddq  7706  caucvgprprlem1  7707  suplocexprlemml  7714  suplocexprlemloc  7719  caucvgsrlemgt1  7793  elreal  7826  axcaucvglemres  7897  axpre-suploc  7900  dfinfre  8911  suprzclex  9349  supinfneg  9593  infsupneg  9594  ublbneg  9611  4fvwrd4  10137  caucvgre  10985  rexanuz  10992  rexfiuz  10993  resqrexlemglsq  11026  resqrexlemsqa  11028  resqrexlemex  11029  rersqreu  11032  clim0  11288  cbvsum  11363  fsum3  11390  mertenslem2  11539  cbvprod  11561  fprodseq  11586  divalgb  11924  infssuzex  11944  bezoutlemmain  11993  bezoutlemex  11996  pythagtriplem2  12260  pythagtriplem19  12276  pythagtrip  12277  pceu  12289  ennnfoneleminc  12406  ennnfonelemex  12409  ennnfonelemr  12418  imasaddfnlemg  12717  tgval2  13444  ntreq0  13525  metrest  13899