Theorem rexbii 2464

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

Syntax hints:   ↔ wb 104  ⊤wtru 1336  ∃wrex 2436

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1427  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-4 1490  ax-17 1506  ax-ial 1514

This theorem depends on definitions:  df-bi 116  df-tru 1338  df-nf 1441  df-rex 2441

This theorem is referenced by:  2rexbii  2466  r19.29r  2595  r19.42v  2614  rexcom13  2622  rexrot4  2623  3reeanv  2627  cbvrex2v  2692  rexcom4  2735  rexcom4a  2736  rexcom4b  2737  ceqsrex2v  2844  clel5  2849  reu7  2907  0el  3416  iuncom  3856  iuncom4  3857  iuniin  3860  dfiunv2  3886  iunab  3896  iunin2  3913  iundif2ss  3915  iunun  3928  iunxiun  3931  iunpwss  3941  inuni  4117  iunopab  4242  sucel  4371  iunpw  4441  xpiundi  4645  xpiundir  4646  reliin  4709  rexxpf  4734  iunxpf  4735  cnvuni  4773  dmiun  4796  dfima3  4932  rniun  4997  dminxp  5031  imaco  5092  coiun  5096  isarep1  5257  rexrn  5605  ralrn  5606  elrnrexdmb  5608  fnasrn  5646  fnasrng  5648  foima2  5703  rexima  5706  ralima  5707  abrexco  5710  imaiun  5711  fliftcnv  5746  abrexex2g  6069  abrexex2  6073  tfr1onlemaccex  6296  tfrcllemaccex  6309  tfrcldm  6311  qsid  6546  eroveu  6572  ixp0  6677  infmoti  6973  eldju  7013  genpdflem  7428  genpassl  7445  genpassu  7446  nqprm  7463  nqprrnd  7464  ltnqpr  7514  ltnqpri  7515  ltexprlemm  7521  ltexprlemopl  7522  ltexprlemopu  7524  caucvgprprlemaddq  7629  caucvgprprlem1  7630  suplocexprlemml  7637  suplocexprlemloc  7642  caucvgsrlemgt1  7716  elreal  7749  axcaucvglemres  7820  axpre-suploc  7823  dfinfre  8828  suprzclex  9263  supinfneg  9507  infsupneg  9508  ublbneg  9523  4fvwrd4  10043  caucvgre  10885  rexanuz  10892  rexfiuz  10893  resqrexlemglsq  10926  resqrexlemsqa  10928  resqrexlemex  10929  rersqreu  10932  clim0  11186  cbvsum  11261  fsum3  11288  mertenslem2  11437  cbvprod  11459  fprodseq  11484  divalgb  11820  infssuzex  11840  bezoutlemmain  11886  bezoutlemex  11889  pythagtriplem2  12145  pythagtriplem19  12161  pythagtrip  12162  ennnfoneleminc  12182  ennnfonelemex  12185  ennnfonelemr  12194  tgval2  12493  ntreq0  12574  metrest  12948