Theorem exbii 1658

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	⊢ (∃𝑥𝜑 ↔ ∃𝑥𝜓)

Proof of Theorem exbii

Step	Hyp	Ref	Expression
1		exbi 1657	. 2 ⊢ (∀𝑥(𝜑 ↔ 𝜓) → (∃𝑥𝜑 ↔ ∃𝑥𝜓))
2		exbii.1	. 2 ⊢ (𝜑 ↔ 𝜓)
3	1, 2	mpg 1504	1 ⊢ (∃𝑥𝜑 ↔ ∃𝑥𝜓)

Syntax hints:   ↔ wb 105  ∃wex 1545

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 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-ial 1587

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  2exbii  1659  3exbii  1660  exancom  1661  excom13  1741  exrot4  1743  eeor  1747  sbcof2  1863  sbequ8  1900  sbidm  1904  sborv  1945  19.41vv  1959  19.41vvv  1960  19.41vvvv  1961  exdistr  1965  19.42vvv  1968  exdistr2  1970  3exdistr  1971  4exdistr  1972  eean  1991  eeeanv  1993  ee4anv  1994  2sb5  2043  2sb5rf  2049  sbel2x  2058  sbexyz  2063  sbex  2064  exsb  2068  2exsb  2069  sb8eu  2099  sb8euh  2109  eu1  2111  eu2  2131  2moswapdc  2177  2exeu  2179  exists1  2183  clelab  2366  clabel  2367  sbabel  2419  rexbii2  2561  r2exf  2568  nfrexdya  2586  r19.41  2706  r19.43  2709  cbvreuvw  2792  isset  2828  rexv  2840  ceqsex2  2863  ceqsex3v  2865  gencbvex  2869  ceqsrexv  2956  rexab  2988  rexrab2  2993  euxfrdc  3012  euind  3013  reu6  3015  reu3  3016  2reuswapdc  3030  reuind  3031  sbccomlem  3126  rmo2ilem  3142  rexun  3409  reupick3  3518  abn0r  3546  abn0m  3547  rabn0m  3549  rexsns  3744  exsnrex  3747  snprc  3770  euabsn2  3776  reusn  3778  eusn  3781  snmb  3829  elunirab  3943  unipr  3944  uniun  3949  uniin  3950  iuncom4  4014  dfiun2g  4039  iunn0m  4068  iunxiun  4089  disjnim  4115  cbvopab2  4200  cbvopab2v  4203  unopab  4205  zfnuleu  4252  0ex  4255  vnex  4259  inex1  4262  intexabim  4283  iinexgm  4285  inuni  4286  unidif0  4299  axpweq  4303  zfpow  4307  axpow2  4308  axpow3  4309  vpwex  4311  zfpair2  4342  mss  4361  exss  4362  opm  4369  eqvinop  4378  copsexg  4379  opabm  4418  iunopab  4419  zfun  4574  uniex2  4576  uniex2OLD  4577  uniuni  4592  rexxfrd  4604  dtruex  4701  zfinf2  4731  elxp2  4787  opeliunxp  4825  xpiundi  4828  xpiundir  4829  elvvv  4833  eliunxp  4914  rexiunxp  4917  relop  4925  elco  4941  opelco2g  4943  cnvco  4960  cnvuni  4961  dfdm3  4962  dfrn2  4963  dfrn3  4964  elrng  4966  dfdm4  4968  eldm2g  4972  dmun  4983  dmin  4984  dmiun  4985  dmuni  4986  dmopab  4987  dmi  4991  reldmm  4995  dmmrnm  4996  elrn  5020  rnopab  5024  dmcosseq  5049  dmres  5079  elres  5094  elsnres  5095  dfima2  5123  elima3  5128  imadmrn  5131  imai  5138  args  5151  rniun  5193  ssrnres  5225  dmsnm  5248  dmsnopg  5254  elxp4  5270  elxp5  5271  cnvresima  5272  mptpreima  5276  dfco2  5282  coundi  5284  coundir  5285  resco  5287  imaco  5288  rnco  5289  coiun  5292  coi1  5298  coass  5301  xpcom  5329  dffun2  5382  imadif  5456  imainlem  5457  funimaexglem  5459  fun11iun  5655  f11o  5668  brprcneu  5683  nfvres  5726  fndmin  5807  abrexco  5955  imaiun  5956  dfoprab2  6125  cbvoprab2  6151  rexrnmpo  6194  opabex3d  6340  opabex3  6341  abexssex  6344  abexex  6345  oprabrexex2  6353  uchoice  6361  releldm2  6409  dfopab2  6413  dfoprab3s  6414  cnvoprab  6460  cnvimadfsn  6475  brtpos2  6512  tfr1onlemaccex  6609  tfrcllembxssdm  6617  tfrcllemaccex  6622  domen  7025  mapsnen  7090  xpsnen  7109  xpcomco  7114  xpassen  7118  fimax2gtri  7196  supelti  7332  cc1  7621  subhalfnqq  7771  ltbtwnnq  7773  prnmaxl  7845  prnminu  7846  prarloc  7860  genpdflem  7864  genpassl  7881  genpassu  7882  ltexprlemm  7957  2rexuz  9961  seq3f1olemp  10930  cbvsum  12104  cbvprod  12303  nnwosdc  12794  4sqlem12  13159  inffinp1  13298  ctiunctal  13310  unct  13311  isbasis2g  15069  tgval2  15075  ntreq0  15156  lmff  15273  metrest  15530  upgrex  16258  1loopgrvd2fi  16460  bj-axempty  16833  bj-axempty2  16834  bj-vprc  16836  bdinex1  16839  bj-zfpair2  16850  bj-uniex2  16856  bj-d0clsepcl  16865