Theorem exbii 1470

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

Syntax hints:   ↔ wb 98  ∃wex 1355

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 1310  ax-gen 1312  ax-ie1 1356  ax-ie2 1357  ax-4 1374  ax-ial 1401

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  2exbii  1471  3exbii  1472  exancom  1473  excom13  1553  exrot4  1555  eeor  1559  sbcof2  1665  sbequ8  1701  sbidm  1705  sborv  1744  19.41vv  1757  19.41vvv  1758  19.41vvvv  1759  exdistr  1761  19.42vvv  1763  exdistr2  1765  3exdistr  1766  4exdistr  1767  eean  1780  eeeanv  1782  ee4anv  1783  2sb5  1833  2sb5rf  1839  sbel2x  1848  sbexyz  1853  sbex  1854  exsb  1858  2exsb  1859  sb8eu  1887  sb8euh  1897  eu1  1899  eu2  1918  2moswapdc  1964  2exeu  1966  exists1  1970  clelab  2136  clabel  2137  sbabel  2177  rexbii2  2305  r2exf  2312  nfrexdya  2329  r19.41  2435  r19.43  2438  isset  2531  rexv  2541  ceqsex2  2563  ceqsex3v  2565  gencbvex  2569  ceqsrexv  2643  rexab  2672  rexrab2  2677  euxfrdc  2696  euind  2697  reu6  2699  reu3  2700  2reuswapdc  2712  reuind  2713  sbccomlem  2801  rmo2ilem  2816  rexun  3092  reupick3  3191  abn0r  3212  rabn0m  3214  rexsns  3373  rexsnsOLD  3374  exsnrex  3377  snprc  3399  euabsn2  3403  reusn  3405  eusn  3408  elunirab  3557  unipr  3558  uniun  3563  uniin  3564  iuncom4  3628  dfiun2g  3653  iunn0m  3681  iunxiun  3700  cbvopab2  3795  cbvopab2v  3798  unopab  3800  zfnuleu  3845  0ex  3848  vprc  3852  inex1  3855  intexabim  3870  iinexgm  3872  inuni  3873  unidif0  3884  axpweq  3888  zfpow  3892  axpow2  3893  axpow3  3894  pwex  3896  zfpair2  3909  mss  3926  exss  3927  opm  3935  eqvinop  3944  copsexg  3945  opabm  3981  iunopab  3982  zfun  4110  uniex2  4112  uniuni  4122  rexxfrd  4134  dtruex  4210  zfinf2  4228  elxp2  4279  opeliunxp  4311  xpiundi  4314  xpiundir  4315  elvvv  4319  eliunxp  4391  rexiunxp  4394  relop  4402  opelco2g  4419  cnvco  4436  cnvuni  4437  dfdm3  4438  dfrn2  4439  dfrn3  4440  elrng  4442  dfdm4  4443  eldm2g  4447  dmun  4458  dmin  4459  dmiun  4460  dmuni  4461  dmopab  4462  dmi  4466  dmmrnm  4470  elrn  4493  rnopab  4497  dmcosseq  4519  dmres  4548  elres  4562  elsnres  4563  dfima2  4586  elima3  4591  imadmrn  4594  imai  4597  args  4610  rniun  4650  ssrnres  4679  dmsnm  4702  dmsnopg  4708  elxp4  4724  elxp5  4725  cnvresima  4726  mptpreima  4730  dfco2  4736  coundi  4738  coundir  4739  resco  4741  imaco  4742  rnco  4743  coiun  4746  coi1  4752  coass  4755  xpcom  4780  dffun2  4828  imadif  4894  imainlem  4895  funimaexglem  4897  fun11iun  5061  f11o  5073  brprcneu  5085  nfvres  5120  fndmin  5188  abrexco  5312  imaiun  5313  dfoprab2  5464  cbvoprab2  5489  rexrnmpt2  5528  opabex3d  5660  opabex3  5661  abexssex  5664  abexex  5665  oprabrexex2  5669  releldm2  5723  dfopab2  5727  dfoprab3s  5728  brtpos2  5777  subhalfnqq  6258  ltbtwnnq  6260  prnmaxl  6329  prnminu  6330  prarloc  6344  genpdflem  6348  genpassl  6366  genpassu  6367  ltexprlemm  6424  bj-vprc  8349  bdinex1  8352  bj-zfpair2  8363  bj-uniex2  8369  bj-d0clsepcl  8382