Theorem rexbii 2539

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

Syntax hints:   ↔ wb 105  ⊤wtru 1398  ∃wrex 2511

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 1495  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-4 1558  ax-17 1574  ax-ial 1582

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-rex 2516

This theorem is referenced by:  2rexbii  2541  r19.29r  2671  r19.42v  2690  rexcom13  2699  rexrot4  2700  3reeanv  2704  cbvrex2vw  2779  cbvrex2v  2781  rexcom4  2826  rexcom4a  2827  rexcom4b  2828  ceqsrex2v  2938  clel5  2943  reu7  3001  0el  3517  iuncom  3976  iuncom4  3977  iuniin  3980  dfiunv2  4006  iunab  4017  iunin2  4034  iundif2ss  4036  iunun  4049  iunxiun  4052  iunpwss  4062  inuni  4245  iunopab  4376  sucel  4507  iunpw  4577  xpiundi  4784  xpiundir  4785  reliin  4849  rexxpf  4877  iunxpf  4878  cnvuni  4916  dmiun  4940  dfima3  5079  rniun  5147  dminxp  5181  imaco  5242  coiun  5246  isarep1  5416  rexrn  5784  ralrn  5785  elrnrexdmb  5787  fnasrn  5826  fnasrng  5828  foima2  5892  rexima  5895  ralima  5896  abrexco  5900  imaiun  5901  fliftcnv  5936  abrexex2g  6282  abrexex2  6286  tfr1onlemaccex  6514  tfrcllemaccex  6527  tfrcldm  6529  qsid  6769  eroveu  6795  ixp0  6900  infmoti  7227  eldju  7267  ficardon  7393  genpdflem  7727  genpassl  7744  genpassu  7745  nqprm  7762  nqprrnd  7763  ltnqpr  7813  ltnqpri  7814  ltexprlemm  7820  ltexprlemopl  7821  ltexprlemopu  7823  caucvgprprlemaddq  7928  caucvgprprlem1  7929  suplocexprlemml  7936  suplocexprlemloc  7941  caucvgsrlemgt1  8015  elreal  8048  axcaucvglemres  8119  axpre-suploc  8122  dfinfre  9136  suprzclex  9578  supinfneg  9829  infsupneg  9830  ublbneg  9847  4fvwrd4  10375  infssuzex  10494  caucvgre  11546  rexanuz  11553  rexfiuz  11554  resqrexlemglsq  11587  resqrexlemsqa  11589  resqrexlemex  11590  rersqreu  11593  clim0  11850  cbvsum  11925  fsum3  11953  mertenslem2  12102  cbvprod  12124  fprodseq  12149  divalgb  12491  bezoutlemmain  12574  bezoutlemex  12577  pythagtriplem2  12844  pythagtriplem19  12860  pythagtrip  12861  pceu  12873  ennnfoneleminc  13037  ennnfonelemex  13040  ennnfonelemr  13049  imasaddfnlemg  13402  tgval2  14781  ntreq0  14862  metrest  15236  plyun0  15466  clwwlknun  16298