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  2643  rexrot4  2644  3reeanv  2648  cbvrex2vw  2717  cbvrex2v  2719  rexcom4  2762  rexcom4a  2763  rexcom4b  2764  ceqsrex2v  2871  clel5  2876  reu7  2934  0el  3447  iuncom  3894  iuncom4  3895  iuniin  3898  dfiunv2  3924  iunab  3935  iunin2  3952  iundif2ss  3954  iunun  3967  iunxiun  3970  iunpwss  3980  inuni  4157  iunopab  4283  sucel  4412  iunpw  4482  xpiundi  4686  xpiundir  4687  reliin  4750  rexxpf  4776  iunxpf  4777  cnvuni  4815  dmiun  4838  dfima3  4975  rniun  5041  dminxp  5075  imaco  5136  coiun  5140  isarep1  5304  rexrn  5655  ralrn  5656  elrnrexdmb  5658  fnasrn  5696  fnasrng  5698  foima2  5754  rexima  5757  ralima  5758  abrexco  5762  imaiun  5763  fliftcnv  5798  abrexex2g  6123  abrexex2  6127  tfr1onlemaccex  6351  tfrcllemaccex  6364  tfrcldm  6366  qsid  6602  eroveu  6628  ixp0  6733  infmoti  7029  eldju  7069  genpdflem  7508  genpassl  7525  genpassu  7526  nqprm  7543  nqprrnd  7544  ltnqpr  7594  ltnqpri  7595  ltexprlemm  7601  ltexprlemopl  7602  ltexprlemopu  7604  caucvgprprlemaddq  7709  caucvgprprlem1  7710  suplocexprlemml  7717  suplocexprlemloc  7722  caucvgsrlemgt1  7796  elreal  7829  axcaucvglemres  7900  axpre-suploc  7903  dfinfre  8915  suprzclex  9353  supinfneg  9597  infsupneg  9598  ublbneg  9615  4fvwrd4  10142  caucvgre  10992  rexanuz  10999  rexfiuz  11000  resqrexlemglsq  11033  resqrexlemsqa  11035  resqrexlemex  11036  rersqreu  11039  clim0  11295  cbvsum  11370  fsum3  11397  mertenslem2  11546  cbvprod  11568  fprodseq  11593  divalgb  11932  infssuzex  11952  bezoutlemmain  12001  bezoutlemex  12004  pythagtriplem2  12268  pythagtriplem19  12284  pythagtrip  12285  pceu  12297  ennnfoneleminc  12414  ennnfonelemex  12417  ennnfonelemr  12426  imasaddfnlemg  12740  tgval2  13590  ntreq0  13671  metrest  14045