Theorem rexbii 2472

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

Syntax hints:   ↔ wb 104  ⊤wtru 1344  ∃wrex 2444

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 1435  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-4 1498  ax-17 1514  ax-ial 1522

This theorem depends on definitions:  df-bi 116  df-tru 1346  df-nf 1449  df-rex 2449

This theorem is referenced by:  2rexbii  2474  r19.29r  2603  r19.42v  2622  rexcom13  2630  rexrot4  2631  3reeanv  2635  cbvrex2vw  2703  cbvrex2v  2705  rexcom4  2748  rexcom4a  2749  rexcom4b  2750  ceqsrex2v  2857  clel5  2862  reu7  2920  0el  3430  iuncom  3871  iuncom4  3872  iuniin  3875  dfiunv2  3901  iunab  3911  iunin2  3928  iundif2ss  3930  iunun  3943  iunxiun  3946  iunpwss  3956  inuni  4133  iunopab  4258  sucel  4387  iunpw  4457  xpiundi  4661  xpiundir  4662  reliin  4725  rexxpf  4750  iunxpf  4751  cnvuni  4789  dmiun  4812  dfima3  4948  rniun  5013  dminxp  5047  imaco  5108  coiun  5112  isarep1  5273  rexrn  5621  ralrn  5622  elrnrexdmb  5624  fnasrn  5662  fnasrng  5664  foima2  5719  rexima  5722  ralima  5723  abrexco  5726  imaiun  5727  fliftcnv  5762  abrexex2g  6085  abrexex2  6089  tfr1onlemaccex  6312  tfrcllemaccex  6325  tfrcldm  6327  qsid  6562  eroveu  6588  ixp0  6693  infmoti  6989  eldju  7029  genpdflem  7444  genpassl  7461  genpassu  7462  nqprm  7479  nqprrnd  7480  ltnqpr  7530  ltnqpri  7531  ltexprlemm  7537  ltexprlemopl  7538  ltexprlemopu  7540  caucvgprprlemaddq  7645  caucvgprprlem1  7646  suplocexprlemml  7653  suplocexprlemloc  7658  caucvgsrlemgt1  7732  elreal  7765  axcaucvglemres  7836  axpre-suploc  7839  dfinfre  8847  suprzclex  9285  supinfneg  9529  infsupneg  9530  ublbneg  9547  4fvwrd4  10071  caucvgre  10919  rexanuz  10926  rexfiuz  10927  resqrexlemglsq  10960  resqrexlemsqa  10962  resqrexlemex  10963  rersqreu  10966  clim0  11222  cbvsum  11297  fsum3  11324  mertenslem2  11473  cbvprod  11495  fprodseq  11520  divalgb  11858  infssuzex  11878  bezoutlemmain  11927  bezoutlemex  11930  pythagtriplem2  12194  pythagtriplem19  12210  pythagtrip  12211  pceu  12223  ennnfoneleminc  12340  ennnfonelemex  12343  ennnfonelemr  12352  tgval2  12651  ntreq0  12732  metrest  13106