Theorem rexbii 2442

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

Syntax hints:   ↔ wb 104  ⊤wtru 1332  ∃wrex 2417

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 1423  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-4 1487  ax-17 1506  ax-ial 1514

This theorem depends on definitions:  df-bi 116  df-tru 1334  df-nf 1437  df-rex 2422

This theorem is referenced by:  2rexbii  2444  r19.29r  2570  r19.42v  2588  rexcom13  2596  rexrot4  2597  3reeanv  2601  cbvrex2v  2666  rexcom4  2709  rexcom4a  2710  rexcom4b  2711  ceqsrex2v  2817  reu7  2879  0el  3385  iuncom  3819  iuncom4  3820  iuniin  3823  dfiunv2  3849  iunab  3859  iunin2  3876  iundif2ss  3878  iunun  3891  iunxiun  3894  iunpwss  3904  inuni  4080  iunopab  4203  sucel  4332  iunpw  4401  xpiundi  4597  xpiundir  4598  reliin  4661  rexxpf  4686  iunxpf  4687  cnvuni  4725  dmiun  4748  dfima3  4884  rniun  4949  dminxp  4983  imaco  5044  coiun  5048  isarep1  5209  rexrn  5557  ralrn  5558  elrnrexdmb  5560  fnasrn  5598  fnasrng  5600  foima2  5653  rexima  5656  ralima  5657  abrexco  5660  imaiun  5661  fliftcnv  5696  abrexex2g  6018  abrexex2  6022  tfr1onlemaccex  6245  tfrcllemaccex  6258  tfrcldm  6260  qsid  6494  eroveu  6520  ixp0  6625  infmoti  6915  eldju  6953  genpdflem  7315  genpassl  7332  genpassu  7333  nqprm  7350  nqprrnd  7351  ltnqpr  7401  ltnqpri  7402  ltexprlemm  7408  ltexprlemopl  7409  ltexprlemopu  7411  caucvgprprlemaddq  7516  caucvgprprlem1  7517  suplocexprlemml  7524  suplocexprlemloc  7529  caucvgsrlemgt1  7603  elreal  7636  axcaucvglemres  7707  axpre-suploc  7710  dfinfre  8714  suprzclex  9149  supinfneg  9390  infsupneg  9391  ublbneg  9405  4fvwrd4  9917  caucvgre  10753  rexanuz  10760  rexfiuz  10761  resqrexlemglsq  10794  resqrexlemsqa  10796  resqrexlemex  10797  rersqreu  10800  clim0  11054  cbvsum  11129  fsum3  11156  mertenslem2  11305  cbvprod  11327  divalgb  11622  infssuzex  11642  bezoutlemmain  11686  bezoutlemex  11689  ennnfoneleminc  11924  ennnfonelemex  11927  ennnfonelemr  11936  tgval2  12220  ntreq0  12301  metrest  12675