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  9247  suprzclex  9694  supinfneg  9945  infsupneg  9946  ublbneg  9963  4fvwrd4  10496  infssuzex  10615  caucvgre  11691  rexanuz  11698  rexfiuz  11699  resqrexlemglsq  11732  resqrexlemsqa  11734  resqrexlemex  11735  rersqreu  11738  clim0  11995  cbvsum  12070  fsum3  12098  mertenslem2  12247  cbvprod  12269  fprodseq  12294  divalgb  12636  bezoutlemmain  12719  bezoutlemex  12722  pythagtriplem2  12989  pythagtriplem19  13005  pythagtrip  13006  pceu  13018  ennnfoneleminc  13246  ennnfonelemex  13249  ennnfonelemr  13258  imasaddfnlemg  13611  tgval2  15028  ntreq0  15109  metrest  15483  plyun0  15713  clwwlknun  16548