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 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐴 𝜓)

This proof depends on syntax axioms:   ↔ wb 105  ⊤wtru 1403  ∃wrex 2529

This proof depends on 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 proof depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-rex 2534

This theorem is used 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  4018  iuncom4  4019  iuniin  4022  dfiunv2  4048  iunab  4059  iunin2  4076  iundif2ss  4078  iunun  4091  iunxiun  4094  iunpwss  4104  inuni  4293  iunopab  4426  sucel  4557  iunpw  4628  xpiundi  4835  xpiundir  4836  reliin  4901  rexxpf  4929  iunxpf  4930  cnvuni  4968  dmiun  4992  dfima3  5132  rniun  5201  dminxp  5235  imaco  5296  coiun  5300  isarep1  5470  rexrn  5848  ralrn  5849  elrnrexdmb  5851  fnasrn  5890  fnasrng  5892  foima2  5960  rexima  5963  ralima  5964  abrexco  5968  imaiun  5969  fliftcnv  6004  abrexex2g  6353  abrexex2  6357  tfr1onlemaccex  6623  tfrcllemaccex  6636  tfrcldm  6638  qsid  6878  eroveu  6904  ixp0  7018  infmoti  7375  eldju  7415  ficardon  7541  genpdflem  7881  genpassl  7898  genpassu  7899  nqprm  7916  nqprrnd  7917  ltnqpr  7967  ltnqpri  7968  ltexprlemm  7974  ltexprlemopl  7975  ltexprlemopu  7977  caucvgprprlemaddq  8082  caucvgprprlem1  8083  suplocexprlemml  8090  suplocexprlemloc  8095  caucvgsrlemgt1  8169  elreal  8202  axcaucvglemres  8273  axpre-suploc  8276  dfinfre  9295  suprzclex  9756  supinfneg  10012  infsupneg  10013  ublbneg  10030  4fvwrd4  10565  infssuzex  10684  caucvgre  11770  rexanuz  11777  rexfiuz  11778  resqrexlemglsq  11811  resqrexlemsqa  11813  resqrexlemex  11814  rersqreu  11817  clim0  12077  cbvsum  12152  fsum3  12180  mertenslem2  12329  cbvprod  12351  fprodseq  12376  divalgb  12718  bezoutlemmain  12801  bezoutlemex  12804  pythagtriplem2  13075  pythagtriplem19  13091  pythagtrip  13092  pceu  13104  ennnfoneleminc  13361  ennnfonelemex  13364  ennnfonelemr  13373  imasaddfnlemg  13695  tgval2  15289  ntreq0  15370  metrest  15744  plyun0  15974  clwwlknun  16899  ralsbii  17361