Theorem rexbii 2477

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

Syntax hints:   ↔ wb 104  ⊤wtru 1349  ∃wrex 2449

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1440  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-4 1503  ax-17 1519  ax-ial 1527

This theorem depends on definitions:  df-bi 116  df-tru 1351  df-nf 1454  df-rex 2454

This theorem is referenced by:  2rexbii  2479  r19.29r  2608  r19.42v  2627  rexcom13  2635  rexrot4  2636  3reeanv  2640  cbvrex2vw  2708  cbvrex2v  2710  rexcom4  2753  rexcom4a  2754  rexcom4b  2755  ceqsrex2v  2862  clel5  2867  reu7  2925  0el  3437  iuncom  3879  iuncom4  3880  iuniin  3883  dfiunv2  3909  iunab  3919  iunin2  3936  iundif2ss  3938  iunun  3951  iunxiun  3954  iunpwss  3964  inuni  4141  iunopab  4266  sucel  4395  iunpw  4465  xpiundi  4669  xpiundir  4670  reliin  4733  rexxpf  4758  iunxpf  4759  cnvuni  4797  dmiun  4820  dfima3  4956  rniun  5021  dminxp  5055  imaco  5116  coiun  5120  isarep1  5284  rexrn  5633  ralrn  5634  elrnrexdmb  5636  fnasrn  5674  fnasrng  5676  foima2  5731  rexima  5734  ralima  5735  abrexco  5738  imaiun  5739  fliftcnv  5774  abrexex2g  6099  abrexex2  6103  tfr1onlemaccex  6327  tfrcllemaccex  6340  tfrcldm  6342  qsid  6578  eroveu  6604  ixp0  6709  infmoti  7005  eldju  7045  genpdflem  7469  genpassl  7486  genpassu  7487  nqprm  7504  nqprrnd  7505  ltnqpr  7555  ltnqpri  7556  ltexprlemm  7562  ltexprlemopl  7563  ltexprlemopu  7565  caucvgprprlemaddq  7670  caucvgprprlem1  7671  suplocexprlemml  7678  suplocexprlemloc  7683  caucvgsrlemgt1  7757  elreal  7790  axcaucvglemres  7861  axpre-suploc  7864  dfinfre  8872  suprzclex  9310  supinfneg  9554  infsupneg  9555  ublbneg  9572  4fvwrd4  10096  caucvgre  10945  rexanuz  10952  rexfiuz  10953  resqrexlemglsq  10986  resqrexlemsqa  10988  resqrexlemex  10989  rersqreu  10992  clim0  11248  cbvsum  11323  fsum3  11350  mertenslem2  11499  cbvprod  11521  fprodseq  11546  divalgb  11884  infssuzex  11904  bezoutlemmain  11953  bezoutlemex  11956  pythagtriplem2  12220  pythagtriplem19  12236  pythagtrip  12237  pceu  12249  ennnfoneleminc  12366  ennnfonelemex  12369  ennnfonelemr  12378  tgval2  12845  ntreq0  12926  metrest  13300