Theorem rexbii 2504

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

Syntax hints:   ↔ wb 105  ⊤wtru 1365  ∃wrex 2476

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 1461  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-4 1524  ax-17 1540  ax-ial 1548

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1475  df-rex 2481

This theorem is referenced by:  2rexbii  2506  r19.29r  2635  r19.42v  2654  rexcom13  2663  rexrot4  2664  3reeanv  2668  cbvrex2vw  2741  cbvrex2v  2743  rexcom4  2786  rexcom4a  2787  rexcom4b  2788  ceqsrex2v  2896  clel5  2901  reu7  2959  0el  3474  iuncom  3923  iuncom4  3924  iuniin  3927  dfiunv2  3953  iunab  3964  iunin2  3981  iundif2ss  3983  iunun  3996  iunxiun  3999  iunpwss  4009  inuni  4189  iunopab  4317  sucel  4446  iunpw  4516  xpiundi  4722  xpiundir  4723  reliin  4786  rexxpf  4814  iunxpf  4815  cnvuni  4853  dmiun  4876  dfima3  5013  rniun  5081  dminxp  5115  imaco  5176  coiun  5180  isarep1  5345  rexrn  5702  ralrn  5703  elrnrexdmb  5705  fnasrn  5743  fnasrng  5745  foima2  5801  rexima  5804  ralima  5805  abrexco  5809  imaiun  5810  fliftcnv  5845  abrexex2g  6186  abrexex2  6190  tfr1onlemaccex  6415  tfrcllemaccex  6428  tfrcldm  6430  qsid  6668  eroveu  6694  ixp0  6799  infmoti  7103  eldju  7143  ficardon  7269  genpdflem  7593  genpassl  7610  genpassu  7611  nqprm  7628  nqprrnd  7629  ltnqpr  7679  ltnqpri  7680  ltexprlemm  7686  ltexprlemopl  7687  ltexprlemopu  7689  caucvgprprlemaddq  7794  caucvgprprlem1  7795  suplocexprlemml  7802  suplocexprlemloc  7807  caucvgsrlemgt1  7881  elreal  7914  axcaucvglemres  7985  axpre-suploc  7988  dfinfre  9002  suprzclex  9443  supinfneg  9688  infsupneg  9689  ublbneg  9706  4fvwrd4  10234  infssuzex  10342  caucvgre  11165  rexanuz  11172  rexfiuz  11173  resqrexlemglsq  11206  resqrexlemsqa  11208  resqrexlemex  11209  rersqreu  11212  clim0  11469  cbvsum  11544  fsum3  11571  mertenslem2  11720  cbvprod  11742  fprodseq  11767  divalgb  12109  bezoutlemmain  12192  bezoutlemex  12195  pythagtriplem2  12462  pythagtriplem19  12478  pythagtrip  12479  pceu  12491  ennnfoneleminc  12655  ennnfonelemex  12658  ennnfonelemr  12667  imasaddfnlemg  13018  tgval2  14395  ntreq0  14476  metrest  14850  plyun0  15080