Theorem exbii 1493

Description: Inference adding existential quantifier to both sides of an equivalence. (Contributed by NM, 24-May-1994.)

Hypothesis

Ref	Expression
exbii.1	⊢ (φ ↔ ψ)

Assertion

Ref	Expression
exbii	⊢ (∃xφ ↔ ∃xψ)

Proof of Theorem exbii

Step	Hyp	Ref	Expression
1		exbi 1492	. 2 ⊢ (∀x(φ ↔ ψ) → (∃xφ ↔ ∃xψ))
2		exbii.1	. 2 ⊢ (φ ↔ ψ)
3	1, 2	mpg 1337	1 ⊢ (∃xφ ↔ ∃xψ)

Syntax hints:   ↔ wb 98  ∃wex 1378

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1333  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-4 1397  ax-ial 1424

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  2exbii  1494  3exbii  1495  exancom  1496  excom13  1576  exrot4  1578  eeor  1582  sbcof2  1688  sbequ8  1724  sbidm  1728  sborv  1767  19.41vv  1780  19.41vvv  1781  19.41vvvv  1782  exdistr  1784  19.42vvv  1786  exdistr2  1788  3exdistr  1789  4exdistr  1790  eean  1803  eeeanv  1805  ee4anv  1806  2sb5  1856  2sb5rf  1862  sbel2x  1871  sbexyz  1876  sbex  1877  exsb  1881  2exsb  1882  sb8eu  1910  sb8euh  1920  eu1  1922  eu2  1941  2moswapdc  1987  2exeu  1989  exists1  1993  clelab  2159  clabel  2160  sbabel  2200  rexbii2  2329  r2exf  2336  nfrexdya  2353  r19.41  2459  r19.43  2462  isset  2555  rexv  2566  ceqsex2  2588  ceqsex3v  2590  gencbvex  2594  ceqsrexv  2668  rexab  2697  rexrab2  2702  euxfrdc  2721  euind  2722  reu6  2724  reu3  2725  2reuswapdc  2737  reuind  2738  sbccomlem  2826  rmo2ilem  2841  rexun  3117  reupick3  3216  abn0r  3237  rabn0m  3239  rexsns  3400  rexsnsOLD  3401  exsnrex  3404  snprc  3426  euabsn2  3430  reusn  3432  eusn  3435  elunirab  3584  unipr  3585  uniun  3590  uniin  3591  iuncom4  3655  dfiun2g  3680  iunn0m  3708  iunxiun  3727  cbvopab2  3822  cbvopab2v  3825  unopab  3827  zfnuleu  3872  0ex  3875  vprc  3879  inex1  3882  intexabim  3897  iinexgm  3899  inuni  3900  unidif0  3911  axpweq  3915  zfpow  3919  axpow2  3920  axpow3  3921  pwex  3923  zfpair2  3936  mss  3953  exss  3954  opm  3962  eqvinop  3971  copsexg  3972  opabm  4008  iunopab  4009  zfun  4137  uniex2  4139  uniuni  4149  rexxfrd  4161  dtruex  4237  zfinf2  4255  elxp2  4306  opeliunxp  4338  xpiundi  4341  xpiundir  4342  elvvv  4346  eliunxp  4418  rexiunxp  4421  relop  4429  opelco2g  4446  cnvco  4463  cnvuni  4464  dfdm3  4465  dfrn2  4466  dfrn3  4467  elrng  4469  dfdm4  4470  eldm2g  4474  dmun  4485  dmin  4486  dmiun  4487  dmuni  4488  dmopab  4489  dmi  4493  dmmrnm  4497  elrn  4520  rnopab  4524  dmcosseq  4546  dmres  4575  elres  4589  elsnres  4590  dfima2  4613  elima3  4618  imadmrn  4621  imai  4624  args  4637  rniun  4677  ssrnres  4706  dmsnm  4729  dmsnopg  4735  elxp4  4751  elxp5  4752  cnvresima  4753  mptpreima  4757  dfco2  4763  coundi  4765  coundir  4766  resco  4768  imaco  4769  rnco  4770  coiun  4773  coi1  4779  coass  4782  xpcom  4807  dffun2  4855  imadif  4922  imainlem  4923  funimaexglem  4925  fun11iun  5090  f11o  5102  brprcneu  5114  nfvres  5149  fndmin  5217  abrexco  5341  imaiun  5342  dfoprab2  5494  cbvoprab2  5519  rexrnmpt2  5558  opabex3d  5690  opabex3  5691  abexssex  5694  abexex  5695  oprabrexex2  5699  releldm2  5753  dfopab2  5757  dfoprab3s  5758  brtpos2  5807  domen  6168  xpsnen  6231  xpcomco  6236  xpassen  6240  subhalfnqq  6397  ltbtwnnq  6399  prnmaxl  6470  prnminu  6471  prarloc  6485  genpdflem  6489  genpassl  6506  genpassu  6507  ltexprlemm  6573  2rexuz  8281  bj-vprc  9327  bdinex1  9330  bj-zfpair2  9341  bj-uniex2  9347  bj-d0clsepcl  9360