Theorem exbii 1480

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 1479	. 2 ⊢ (∀x(φ ↔ ψ) → (∃xφ ↔ ∃xψ))
2		exbii.1	. 2 ⊢ (φ ↔ ψ)
3	1, 2	mpg 1320	1 ⊢ (∃xφ ↔ ∃xψ)

Syntax hints:   ↔ wb 98  ∃wex 1362

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 1316  ax-gen 1318  ax-ie1 1363  ax-ie2 1364  ax-4 1383  ax-ial 1411

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  2exbii  1481  3exbii  1482  exancom  1483  excom13  1561  exrot4  1563  eeor  1567  sbcof2  1674  sbequ8  1710  sbidm  1715  sborv  1754  19.41vv  1767  19.41vvv  1768  19.41vvvv  1769  exdistr  1771  19.42vvv  1773  exdistr2  1774  3exdistr  1775  4exdistr  1776  eean  1789  eeeanv  1791  ee4anv  1792  2sb5  1841  2sb5rf  1847  sbel2x  1856  sbexyz  1861  sbex  1862  exsb  1866  2exsb  1867  sb8eu  1895  sb8euh  1905  eu1  1907  eu2  1926  2moswapdc  1973  2exeu  1975  exists1  1979  clelab  2145  clabel  2146  sbabel  2186  rexbii2  2312  r2exf  2319  nfrexdya  2336  r19.41  2442  r19.43  2445  isset  2538  rexv  2548  ceqsex2  2570  ceqsex3v  2572  gencbvex  2576  ceqsrexv  2650  rexab  2679  rexrab2  2684  euxfrdc  2703  euind  2704  reu6  2706  reu3  2707  2reuswapdc  2719  reuind  2720  sbccomlem  2809  rmo2ilem  2824  rexun  3102  reupick3  3201  abn0r  3222  rabn0m  3224  rexsns  3361  rexsnsOLD  3362  exsnrex  3365  snprc  3387  euabsn2  3391  reusn  3393  eusn  3396  elunirab  3546  unipr  3547  uniun  3552  uniin  3553  iuncom4  3617  dfiun2g  3642  iunn0m  3670  iunxiun  3689  cbvopab2  3784  cbvopab2v  3787  unopab  3789  zfnuleu  3834  0ex  3837  vprc  3841  inex1  3844  intexabim  3859  iinexgm  3861  inuni  3862  unidif0  3873  axpweq  3877  zfpow  3881  axpow2  3882  axpow3  3883  pwex  3885  zfpair2  3898  mss  3915  exss  3916  opm  3924  eqvinop  3933  copsexg  3934  opabm  3971  iunopab  3972  zfun  4097  uniex2  4099  uniuni  4109  rexxfrd  4121  dtruex  4197  zfinf2  4215  elxp2  4266  opeliunxp  4298  xpiundi  4301  xpiundir  4302  elvvv  4306  eliunxp  4378  rexiunxp  4381  relop  4389  opelco2g  4406  cnvco  4423  cnvuni  4424  dfdm3  4425  dfrn2  4426  dfrn3  4427  elrng  4429  dfdm4  4430  eldm2g  4434  dmun  4445  dmin  4446  dmiun  4447  dmuni  4448  dmopab  4449  dmi  4453  dmmrnm  4457  elrn  4480  rnopab  4484  dmcosseq  4506  dmres  4536  elres  4550  elsnres  4551  dfima2  4574  elima3  4579  imadmrn  4582  imai  4585  args  4598  rniun  4638  ssrnres  4667  dmsnm  4690  dmsnopg  4696  elxp4  4712  elxp5  4713  cnvresima  4714  mptpreima  4718  dfco2  4724  coundi  4726  coundir  4727  resco  4729  imaco  4730  rnco  4731  coiun  4734  coi1  4740  coass  4743  xpcom  4768  dffun2  4816  imadif  4882  imainlem  4883  funimaexglem  4885  fun11iun  5049  f11o  5061  brprcneu  5073  nfvres  5108  fndmin  5176  abrexco  5300  imaiun  5301  dfoprab2  5454  cbvoprab2  5479  rexrnmpt2  5518  opabex3d  5647  opabex3  5648  abexssex  5651  abexex  5652  oprabrexex2  5656  releldm2  5710  dfopab2  5714  dfoprab3s  5715  brtpos2  5764