Theorem rexbii 2551

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

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

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 2528

This theorem is referenced by:  2rexbii  2553  r19.29r  2683  r19.42v  2702  rexcom13  2711  rexrot4  2712  3reeanv  2716  cbvrex2vw  2792  cbvrex2v  2794  rexcom4  2839  rexcom4a  2840  rexcom4b  2841  ceqsrex2v  2952  clel5  2957  reu7  3015  0el  3535  iuncom  4002  iuncom4  4003  iuniin  4006  dfiunv2  4032  iunab  4043  iunin2  4060  iundif2ss  4062  iunun  4075  iunxiun  4078  iunpwss  4088  inuni  4272  iunopab  4405  sucel  4536  iunpw  4606  xpiundi  4813  xpiundir  4814  reliin  4879  rexxpf  4907  iunxpf  4908  cnvuni  4946  dmiun  4970  dfima3  5109  rniun  5178  dminxp  5212  imaco  5273  coiun  5277  isarep1  5447  rexrn  5819  ralrn  5820  elrnrexdmb  5822  fnasrn  5861  fnasrng  5863  foima2  5930  rexima  5933  ralima  5934  abrexco  5938  imaiun  5939  fliftcnv  5974  abrexex2g  6322  abrexex2  6326  tfr1onlemaccex  6592  tfrcllemaccex  6605  tfrcldm  6607  qsid  6847  eroveu  6873  ixp0  6979  infmoti  7332  eldju  7372  ficardon  7498  genpdflem  7838  genpassl  7855  genpassu  7856  nqprm  7873  nqprrnd  7874  ltnqpr  7924  ltnqpri  7925  ltexprlemm  7931  ltexprlemopl  7932  ltexprlemopu  7934  caucvgprprlemaddq  8039  caucvgprprlem1  8040  suplocexprlemml  8047  suplocexprlemloc  8052  caucvgsrlemgt1  8126  elreal  8159  axcaucvglemres  8230  axpre-suploc  8233  dfinfre  9250  suprzclex  9697  supinfneg  9948  infsupneg  9949  ublbneg  9966  4fvwrd4  10499  infssuzex  10618  caucvgre  11695  rexanuz  11702  rexfiuz  11703  resqrexlemglsq  11736  resqrexlemsqa  11738  resqrexlemex  11739  rersqreu  11742  clim0  11999  cbvsum  12074  fsum3  12102  mertenslem2  12251  cbvprod  12273  fprodseq  12298  divalgb  12640  bezoutlemmain  12723  bezoutlemex  12726  pythagtriplem2  12993  pythagtriplem19  13009  pythagtrip  13010  pceu  13022  ennnfoneleminc  13250  ennnfonelemex  13253  ennnfonelemr  13262  imasaddfnlemg  13582  tgval2  15046  ntreq0  15127  metrest  15501  plyun0  15731  clwwlknun  16566