Theorem exbii 1616

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 1615	. 2 ⊢ (∀𝑥(𝜑 ↔ 𝜓) → (∃𝑥𝜑 ↔ ∃𝑥𝜓))
2		exbii.1	. 2 ⊢ (𝜑 ↔ 𝜓)
3	1, 2	mpg 1462	1 ⊢ (∃𝑥𝜑 ↔ ∃𝑥𝜓)

Syntax hints:   ↔ wb 105  ∃wex 1503

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 1458  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-4 1521  ax-ial 1545

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  2exbii  1617  3exbii  1618  exancom  1619  excom13  1700  exrot4  1702  eeor  1706  sbcof2  1821  sbequ8  1858  sbidm  1862  sborv  1902  19.41vv  1915  19.41vvv  1916  19.41vvvv  1917  exdistr  1921  19.42vvv  1924  exdistr2  1926  3exdistr  1927  4exdistr  1928  eean  1943  eeeanv  1945  ee4anv  1946  2sb5  1995  2sb5rf  2001  sbel2x  2010  sbexyz  2015  sbex  2016  exsb  2020  2exsb  2021  sb8eu  2051  sb8euh  2061  eu1  2063  eu2  2082  2moswapdc  2128  2exeu  2130  exists1  2134  clelab  2315  clabel  2316  sbabel  2359  rexbii2  2501  r2exf  2508  nfrexdya  2526  r19.41  2645  r19.43  2648  cbvreuvw  2724  isset  2758  rexv  2770  ceqsex2  2792  ceqsex3v  2794  gencbvex  2798  ceqsrexv  2882  rexab  2914  rexrab2  2919  euxfrdc  2938  euind  2939  reu6  2941  reu3  2942  2reuswapdc  2956  reuind  2957  sbccomlem  3052  rmo2ilem  3067  rexun  3330  reupick3  3435  abn0r  3462  abn0m  3463  rabn0m  3465  rexsns  3646  exsnrex  3649  snprc  3672  euabsn2  3676  reusn  3678  eusn  3681  elunirab  3837  unipr  3838  uniun  3843  uniin  3844  iuncom4  3908  dfiun2g  3933  iunn0m  3962  iunxiun  3983  disjnim  4009  cbvopab2  4092  cbvopab2v  4095  unopab  4097  zfnuleu  4142  0ex  4145  vnex  4149  inex1  4152  intexabim  4167  iinexgm  4169  inuni  4170  unidif0  4182  axpweq  4186  zfpow  4190  axpow2  4191  axpow3  4192  vpwex  4194  zfpair2  4225  mss  4241  exss  4242  opm  4249  eqvinop  4258  copsexg  4259  opabm  4295  iunopab  4296  zfun  4449  uniex2  4451  uniuni  4466  rexxfrd  4478  dtruex  4573  zfinf2  4603  elxp2  4659  opeliunxp  4696  xpiundi  4699  xpiundir  4700  elvvv  4704  eliunxp  4781  rexiunxp  4784  relop  4792  elco  4808  opelco2g  4810  cnvco  4827  cnvuni  4828  dfdm3  4829  dfrn2  4830  dfrn3  4831  elrng  4833  dfdm4  4834  eldm2g  4838  dmun  4849  dmin  4850  dmiun  4851  dmuni  4852  dmopab  4853  dmi  4857  dmmrnm  4861  elrn  4885  rnopab  4889  dmcosseq  4913  dmres  4943  elres  4958  elsnres  4959  dfima2  4987  elima3  4992  imadmrn  4995  imai  4999  args  5012  rniun  5054  ssrnres  5086  dmsnm  5109  dmsnopg  5115  elxp4  5131  elxp5  5132  cnvresima  5133  mptpreima  5137  dfco2  5143  coundi  5145  coundir  5146  resco  5148  imaco  5149  rnco  5150  coiun  5153  coi1  5159  coass  5162  xpcom  5190  dffun2  5242  imadif  5312  imainlem  5313  funimaexglem  5315  fun11iun  5498  f11o  5510  brprcneu  5524  nfvres  5564  fndmin  5640  abrexco  5777  imaiun  5778  dfoprab2  5939  cbvoprab2  5965  rexrnmpo  6008  opabex3d  6141  opabex3  6142  abexssex  6145  abexex  6146  oprabrexex2  6150  releldm2  6205  dfopab2  6209  dfoprab3s  6210  cnvoprab  6254  brtpos2  6271  tfr1onlemaccex  6368  tfrcllembxssdm  6376  tfrcllemaccex  6381  domen  6772  mapsnen  6832  xpsnen  6842  xpcomco  6847  xpassen  6851  fimax2gtri  6924  supelti  7026  cc1  7289  subhalfnqq  7438  ltbtwnnq  7440  prnmaxl  7512  prnminu  7513  prarloc  7527  genpdflem  7531  genpassl  7548  genpassu  7549  ltexprlemm  7624  2rexuz  9607  seq3f1olemp  10528  cbvsum  11395  cbvprod  11593  nnwosdc  12067  4sqlem12  12429  inffinp1  12475  ctiunctal  12487  unct  12488  isbasis2g  13982  tgval2  13988  ntreq0  14069  lmff  14186  metrest  14443  bj-axempty  15082  bj-axempty2  15083  bj-vprc  15085  bdinex1  15088  bj-zfpair2  15099  bj-uniex2  15105  bj-d0clsepcl  15114