Theorem exbii 1478

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 1477	. 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 1381  ax-ial 1409

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  2exbii  1479  3exbii  1480  exancom  1481  excom13  1561  exrot4  1563  eeor  1567  sbcof2  1673  sbequ8  1709  sbidm  1713  sborv  1752  19.41vv  1765  19.41vvv  1766  19.41vvvv  1767  exdistr  1769  19.42vvv  1771  exdistr2  1773  3exdistr  1774  4exdistr  1775  eean  1788  eeeanv  1790  ee4anv  1791  2sb5  1841  2sb5rf  1847  sbel2x  1856  sbexyz  1861  sbex  1862  exsb  1866  2exsb  1867  sb8eu  1895  sb8euh  1905  eu1  1907  eu2  1926  2moswapdc  1972  2exeu  1974  exists1  1978  clelab  2144  clabel  2145  sbabel  2185  rexbii2  2313  r2exf  2320  nfrexdya  2337  r19.41  2443  r19.43  2446  isset  2539  rexv  2549  ceqsex2  2571  ceqsex3v  2573  gencbvex  2577  ceqsrexv  2651  rexab  2680  rexrab2  2685  euxfrdc  2704  euind  2705  reu6  2707  reu3  2708  2reuswapdc  2720  reuind  2721  sbccomlem  2809  rmo2ilem  2824  rexun  3100  reupick3  3199  abn0r  3220  rabn0m  3222  rexsns  3383  rexsnsOLD  3384  exsnrex  3387  snprc  3409  euabsn2  3413  reusn  3415  eusn  3418  elunirab  3567  unipr  3568  uniun  3573  uniin  3574  iuncom4  3638  dfiun2g  3663  iunn0m  3691  iunxiun  3710  cbvopab2  3805  cbvopab2v  3808  unopab  3810  zfnuleu  3855  0ex  3858  vprc  3862  inex1  3865  intexabim  3880  iinexgm  3882  inuni  3883  unidif0  3894  axpweq  3898  zfpow  3902  axpow2  3903  axpow3  3904  pwex  3906  zfpair2  3919  mss  3936  exss  3937  opm  3945  eqvinop  3954  copsexg  3955  opabm  3991  iunopab  3992  zfun  4121  uniex2  4123  uniuni  4133  rexxfrd  4145  dtruex  4221  zfinf2  4239  elxp2  4290  opeliunxp  4322  xpiundi  4325  xpiundir  4326  elvvv  4330  eliunxp  4402  rexiunxp  4405  relop  4413  opelco2g  4430  cnvco  4447  cnvuni  4448  dfdm3  4449  dfrn2  4450  dfrn3  4451  elrng  4453  dfdm4  4454  eldm2g  4458  dmun  4469  dmin  4470  dmiun  4471  dmuni  4472  dmopab  4473  dmi  4477  dmmrnm  4481  elrn  4504  rnopab  4508  dmcosseq  4530  dmres  4559  elres  4573  elsnres  4574  dfima2  4597  elima3  4602  imadmrn  4605  imai  4608  args  4621  rniun  4661  ssrnres  4690  dmsnm  4713  dmsnopg  4719  elxp4  4735  elxp5  4736  cnvresima  4737  mptpreima  4741  dfco2  4747  coundi  4749  coundir  4750  resco  4752  imaco  4753  rnco  4754  coiun  4757  coi1  4763  coass  4766  xpcom  4791  dffun2  4839  imadif  4905  imainlem  4906  funimaexglem  4908  fun11iun  5072  f11o  5084  brprcneu  5096  nfvres  5131  fndmin  5199  abrexco  5323  imaiun  5324  dfoprab2  5475  cbvoprab2  5500  rexrnmpt2  5539  opabex3d  5671  opabex3  5672  abexssex  5675  abexex  5676  oprabrexex2  5680  releldm2  5734  dfopab2  5738  dfoprab3s  5739  brtpos2  5788  subhalfnqq  6271  ltbtwnnq  6273  prnmaxl  6342  prnminu  6343  prarloc  6357  genpdflem  6361  genpassl  6379  genpassu  6380  ltexprlemm  6437  bj-vprc  7119  bdinex1  7122  bj-zfpair2  7133  bj-uniex2  7139  bj-d0clsepcl  7148