Theorem rexbii 2549

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

Syntax hints:   ↔ wb 105  ⊤wtru 1399  ∃wrex 2521

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 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-17 1575  ax-ial 1583

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-rex 2526

This theorem is referenced by:  2rexbii  2551  r19.29r  2681  r19.42v  2700  rexcom13  2709  rexrot4  2710  3reeanv  2714  cbvrex2vw  2789  cbvrex2v  2791  rexcom4  2836  rexcom4a  2837  rexcom4b  2838  ceqsrex2v  2948  clel5  2953  reu7  3011  0el  3530  iuncom  3996  iuncom4  3997  iuniin  4000  dfiunv2  4026  iunab  4037  iunin2  4054  iundif2ss  4056  iunun  4069  iunxiun  4072  iunpwss  4082  inuni  4266  iunopab  4399  sucel  4530  iunpw  4600  xpiundi  4807  xpiundir  4808  reliin  4873  rexxpf  4901  iunxpf  4902  cnvuni  4940  dmiun  4964  dfima3  5103  rniun  5172  dminxp  5206  imaco  5267  coiun  5271  isarep1  5441  rexrn  5813  ralrn  5814  elrnrexdmb  5816  fnasrn  5855  fnasrng  5857  foima2  5923  rexima  5926  ralima  5927  abrexco  5931  imaiun  5932  fliftcnv  5967  abrexex2g  6312  abrexex2  6316  tfr1onlemaccex  6578  tfrcllemaccex  6591  tfrcldm  6593  qsid  6833  eroveu  6859  ixp0  6965  infmoti  7318  eldju  7358  ficardon  7484  genpdflem  7821  genpassl  7838  genpassu  7839  nqprm  7856  nqprrnd  7857  ltnqpr  7907  ltnqpri  7908  ltexprlemm  7914  ltexprlemopl  7915  ltexprlemopu  7917  caucvgprprlemaddq  8022  caucvgprprlem1  8023  suplocexprlemml  8030  suplocexprlemloc  8035  caucvgsrlemgt1  8109  elreal  8142  axcaucvglemres  8213  axpre-suploc  8216  dfinfre  9229  suprzclex  9675  supinfneg  9926  infsupneg  9927  ublbneg  9944  4fvwrd4  10473  infssuzex  10592  caucvgre  11662  rexanuz  11669  rexfiuz  11670  resqrexlemglsq  11703  resqrexlemsqa  11705  resqrexlemex  11706  rersqreu  11709  clim0  11966  cbvsum  12041  fsum3  12069  mertenslem2  12218  cbvprod  12240  fprodseq  12265  divalgb  12607  bezoutlemmain  12690  bezoutlemex  12693  pythagtriplem2  12960  pythagtriplem19  12976  pythagtrip  12977  pceu  12989  ennnfoneleminc  13154  ennnfonelemex  13157  ennnfonelemr  13166  imasaddfnlemg  13519  tgval2  14908  ntreq0  14989  metrest  15363  plyun0  15593  clwwlknun  16428