Theorem rexbii 2557

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

Syntax hints:   ↔ wb 105  ⊤wtru 1403  ∃wrex 2529

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 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-17 1579  ax-ial 1587

This theorem depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-rex 2534

This theorem is referenced by:  2rexbii  2559  r19.29r  2689  r19.42v  2708  rexcom13  2717  rexrot4  2718  3reeanv  2722  cbvrex2vw  2798  cbvrex2v  2800  rexcom4  2845  rexcom4a  2846  rexcom4b  2847  ceqsrex2v  2958  clel5  2963  reu7  3021  0el  3544  iuncom  4016  iuncom4  4017  iuniin  4020  dfiunv2  4046  iunab  4057  iunin2  4074  iundif2ss  4076  iunun  4089  iunxiun  4092  iunpwss  4102  inuni  4289  iunopab  4422  sucel  4553  iunpw  4624  xpiundi  4831  xpiundir  4832  reliin  4897  rexxpf  4925  iunxpf  4926  cnvuni  4964  dmiun  4988  dfima3  5127  rniun  5196  dminxp  5230  imaco  5291  coiun  5295  isarep1  5465  rexrn  5839  ralrn  5840  elrnrexdmb  5842  fnasrn  5881  fnasrng  5883  foima2  5951  rexima  5954  ralima  5955  abrexco  5959  imaiun  5960  fliftcnv  5995  abrexex2g  6343  abrexex2  6347  tfr1onlemaccex  6613  tfrcllemaccex  6626  tfrcldm  6628  qsid  6868  eroveu  6894  ixp0  7007  infmoti  7362  eldju  7402  ficardon  7528  genpdflem  7868  genpassl  7885  genpassu  7886  nqprm  7903  nqprrnd  7904  ltnqpr  7954  ltnqpri  7955  ltexprlemm  7961  ltexprlemopl  7962  ltexprlemopu  7964  caucvgprprlemaddq  8069  caucvgprprlem1  8070  suplocexprlemml  8077  suplocexprlemloc  8082  caucvgsrlemgt1  8156  elreal  8189  axcaucvglemres  8260  axpre-suploc  8263  dfinfre  9280  suprzclex  9727  supinfneg  9978  infsupneg  9979  ublbneg  9996  4fvwrd4  10530  infssuzex  10649  caucvgre  11730  rexanuz  11737  rexfiuz  11738  resqrexlemglsq  11771  resqrexlemsqa  11773  resqrexlemex  11774  rersqreu  11777  clim0  12034  cbvsum  12109  fsum3  12137  mertenslem2  12286  cbvprod  12308  fprodseq  12333  divalgb  12675  bezoutlemmain  12758  bezoutlemex  12761  pythagtriplem2  13028  pythagtriplem19  13044  pythagtrip  13045  pceu  13057  ennnfoneleminc  13285  ennnfonelemex  13288  ennnfonelemr  13297  imasaddfnlemg  13618  tgval2  15135  ntreq0  15216  metrest  15590  plyun0  15820  clwwlknun  16665  ralsbii  17116