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  3473  iuncom  3922  iuncom4  3923  iuniin  3926  dfiunv2  3952  iunab  3963  iunin2  3980  iundif2ss  3982  iunun  3995  iunxiun  3998  iunpwss  4008  inuni  4188  iunopab  4316  sucel  4445  iunpw  4515  xpiundi  4721  xpiundir  4722  reliin  4785  rexxpf  4813  iunxpf  4814  cnvuni  4852  dmiun  4875  dfima3  5012  rniun  5080  dminxp  5114  imaco  5175  coiun  5179  isarep1  5344  rexrn  5699  ralrn  5700  elrnrexdmb  5702  fnasrn  5740  fnasrng  5742  foima2  5798  rexima  5801  ralima  5802  abrexco  5806  imaiun  5807  fliftcnv  5842  abrexex2g  6177  abrexex2  6181  tfr1onlemaccex  6406  tfrcllemaccex  6419  tfrcldm  6421  qsid  6659  eroveu  6685  ixp0  6790  infmoti  7094  eldju  7134  genpdflem  7574  genpassl  7591  genpassu  7592  nqprm  7609  nqprrnd  7610  ltnqpr  7660  ltnqpri  7661  ltexprlemm  7667  ltexprlemopl  7668  ltexprlemopu  7670  caucvgprprlemaddq  7775  caucvgprprlem1  7776  suplocexprlemml  7783  suplocexprlemloc  7788  caucvgsrlemgt1  7862  elreal  7895  axcaucvglemres  7966  axpre-suploc  7969  dfinfre  8983  suprzclex  9424  supinfneg  9669  infsupneg  9670  ublbneg  9687  4fvwrd4  10215  infssuzex  10323  caucvgre  11146  rexanuz  11153  rexfiuz  11154  resqrexlemglsq  11187  resqrexlemsqa  11189  resqrexlemex  11190  rersqreu  11193  clim0  11450  cbvsum  11525  fsum3  11552  mertenslem2  11701  cbvprod  11723  fprodseq  11748  divalgb  12090  bezoutlemmain  12165  bezoutlemex  12168  pythagtriplem2  12435  pythagtriplem19  12451  pythagtrip  12452  pceu  12464  ennnfoneleminc  12628  ennnfonelemex  12631  ennnfonelemr  12640  imasaddfnlemg  12957  tgval2  14287  ntreq0  14368  metrest  14742  plyun0  14972