Theorem rexbii 2504

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

Syntax hints:   ↔ wb 105  ⊤wtru 1365  ∃wrex 2476

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 1461  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-4 1524  ax-17 1540  ax-ial 1548

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1475  df-rex 2481

This theorem is referenced by:  2rexbii  2506  r19.29r  2635  r19.42v  2654  rexcom13  2663  rexrot4  2664  3reeanv  2668  cbvrex2vw  2741  cbvrex2v  2743  rexcom4  2786  rexcom4a  2787  rexcom4b  2788  ceqsrex2v  2896  clel5  2901  reu7  2959  0el  3474  iuncom  3923  iuncom4  3924  iuniin  3927  dfiunv2  3953  iunab  3964  iunin2  3981  iundif2ss  3983  iunun  3996  iunxiun  3999  iunpwss  4009  inuni  4189  iunopab  4317  sucel  4446  iunpw  4516  xpiundi  4722  xpiundir  4723  reliin  4786  rexxpf  4814  iunxpf  4815  cnvuni  4853  dmiun  4876  dfima3  5013  rniun  5081  dminxp  5115  imaco  5176  coiun  5180  isarep1  5345  rexrn  5702  ralrn  5703  elrnrexdmb  5705  fnasrn  5743  fnasrng  5745  foima2  5801  rexima  5804  ralima  5805  abrexco  5809  imaiun  5810  fliftcnv  5845  abrexex2g  6186  abrexex2  6190  tfr1onlemaccex  6415  tfrcllemaccex  6428  tfrcldm  6430  qsid  6668  eroveu  6694  ixp0  6799  infmoti  7103  eldju  7143  ficardon  7267  genpdflem  7591  genpassl  7608  genpassu  7609  nqprm  7626  nqprrnd  7627  ltnqpr  7677  ltnqpri  7678  ltexprlemm  7684  ltexprlemopl  7685  ltexprlemopu  7687  caucvgprprlemaddq  7792  caucvgprprlem1  7793  suplocexprlemml  7800  suplocexprlemloc  7805  caucvgsrlemgt1  7879  elreal  7912  axcaucvglemres  7983  axpre-suploc  7986  dfinfre  9000  suprzclex  9441  supinfneg  9686  infsupneg  9687  ublbneg  9704  4fvwrd4  10232  infssuzex  10340  caucvgre  11163  rexanuz  11170  rexfiuz  11171  resqrexlemglsq  11204  resqrexlemsqa  11206  resqrexlemex  11207  rersqreu  11210  clim0  11467  cbvsum  11542  fsum3  11569  mertenslem2  11718  cbvprod  11740  fprodseq  11765  divalgb  12107  bezoutlemmain  12190  bezoutlemex  12193  pythagtriplem2  12460  pythagtriplem19  12476  pythagtrip  12477  pceu  12489  ennnfoneleminc  12653  ennnfonelemex  12656  ennnfonelemr  12665  imasaddfnlemg  13016  tgval2  14371  ntreq0  14452  metrest  14826  plyun0  15056