Theorem rexbii 2537

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

Syntax hints:   ↔ wb 105  ⊤wtru 1396  ∃wrex 2509

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 1493  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-4 1556  ax-17 1572  ax-ial 1580

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-rex 2514

This theorem is referenced by:  2rexbii  2539  r19.29r  2669  r19.42v  2688  rexcom13  2697  rexrot4  2698  3reeanv  2702  cbvrex2vw  2777  cbvrex2v  2779  rexcom4  2824  rexcom4a  2825  rexcom4b  2826  ceqsrex2v  2936  clel5  2941  reu7  2999  0el  3515  iuncom  3974  iuncom4  3975  iuniin  3978  dfiunv2  4004  iunab  4015  iunin2  4032  iundif2ss  4034  iunun  4047  iunxiun  4050  iunpwss  4060  inuni  4243  iunopab  4374  sucel  4505  iunpw  4575  xpiundi  4782  xpiundir  4783  reliin  4847  rexxpf  4875  iunxpf  4876  cnvuni  4914  dmiun  4938  dfima3  5077  rniun  5145  dminxp  5179  imaco  5240  coiun  5244  isarep1  5413  rexrn  5780  ralrn  5781  elrnrexdmb  5783  fnasrn  5821  fnasrng  5823  foima2  5887  rexima  5890  ralima  5891  abrexco  5895  imaiun  5896  fliftcnv  5931  abrexex2g  6277  abrexex2  6281  tfr1onlemaccex  6509  tfrcllemaccex  6522  tfrcldm  6524  qsid  6764  eroveu  6790  ixp0  6895  infmoti  7221  eldju  7261  ficardon  7387  genpdflem  7720  genpassl  7737  genpassu  7738  nqprm  7755  nqprrnd  7756  ltnqpr  7806  ltnqpri  7807  ltexprlemm  7813  ltexprlemopl  7814  ltexprlemopu  7816  caucvgprprlemaddq  7921  caucvgprprlem1  7922  suplocexprlemml  7929  suplocexprlemloc  7934  caucvgsrlemgt1  8008  elreal  8041  axcaucvglemres  8112  axpre-suploc  8115  dfinfre  9129  suprzclex  9571  supinfneg  9822  infsupneg  9823  ublbneg  9840  4fvwrd4  10368  infssuzex  10486  caucvgre  11535  rexanuz  11542  rexfiuz  11543  resqrexlemglsq  11576  resqrexlemsqa  11578  resqrexlemex  11579  rersqreu  11582  clim0  11839  cbvsum  11914  fsum3  11941  mertenslem2  12090  cbvprod  12112  fprodseq  12137  divalgb  12479  bezoutlemmain  12562  bezoutlemex  12565  pythagtriplem2  12832  pythagtriplem19  12848  pythagtrip  12849  pceu  12861  ennnfoneleminc  13025  ennnfonelemex  13028  ennnfonelemr  13037  imasaddfnlemg  13390  tgval2  14768  ntreq0  14849  metrest  15223  plyun0  15453  clwwlknun  16250