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  1947  eeeanv  1949  ee4anv  1950  2sb5  1999  2sb5rf  2005  sbel2x  2014  sbexyz  2019  sbex  2020  exsb  2024  2exsb  2025  sb8eu  2055  sb8euh  2065  eu1  2067  eu2  2086  2moswapdc  2132  2exeu  2134  exists1  2138  clelab  2319  clabel  2320  sbabel  2363  rexbii2  2505  r2exf  2512  nfrexdya  2530  r19.41  2649  r19.43  2652  cbvreuvw  2732  isset  2766  rexv  2778  ceqsex2  2801  ceqsex3v  2803  gencbvex  2807  ceqsrexv  2891  rexab  2923  rexrab2  2928  euxfrdc  2947  euind  2948  reu6  2950  reu3  2951  2reuswapdc  2965  reuind  2966  sbccomlem  3061  rmo2ilem  3076  rexun  3340  reupick3  3445  abn0r  3472  abn0m  3473  rabn0m  3475  rexsns  3658  exsnrex  3661  snprc  3684  euabsn2  3688  reusn  3690  eusn  3693  elunirab  3849  unipr  3850  uniun  3855  uniin  3856  iuncom4  3920  dfiun2g  3945  iunn0m  3974  iunxiun  3995  disjnim  4021  cbvopab2  4104  cbvopab2v  4107  unopab  4109  zfnuleu  4154  0ex  4157  vnex  4161  inex1  4164  intexabim  4182  iinexgm  4184  inuni  4185  unidif0  4197  axpweq  4201  zfpow  4205  axpow2  4206  axpow3  4207  vpwex  4209  zfpair2  4240  mss  4256  exss  4257  opm  4264  eqvinop  4273  copsexg  4274  opabm  4312  iunopab  4313  zfun  4466  uniex2  4468  uniuni  4483  rexxfrd  4495  dtruex  4592  zfinf2  4622  elxp2  4678  opeliunxp  4715  xpiundi  4718  xpiundir  4719  elvvv  4723  eliunxp  4802  rexiunxp  4805  relop  4813  elco  4829  opelco2g  4831  cnvco  4848  cnvuni  4849  dfdm3  4850  dfrn2  4851  dfrn3  4852  elrng  4854  dfdm4  4855  eldm2g  4859  dmun  4870  dmin  4871  dmiun  4872  dmuni  4873  dmopab  4874  dmi  4878  dmmrnm  4882  elrn  4906  rnopab  4910  dmcosseq  4934  dmres  4964  elres  4979  elsnres  4980  dfima2  5008  elima3  5013  imadmrn  5016  imai  5022  args  5035  rniun  5077  ssrnres  5109  dmsnm  5132  dmsnopg  5138  elxp4  5154  elxp5  5155  cnvresima  5156  mptpreima  5160  dfco2  5166  coundi  5168  coundir  5169  resco  5171  imaco  5172  rnco  5173  coiun  5176  coi1  5182  coass  5185  xpcom  5213  dffun2  5265  imadif  5335  imainlem  5336  funimaexglem  5338  fun11iun  5522  f11o  5534  brprcneu  5548  nfvres  5589  fndmin  5666  abrexco  5803  imaiun  5804  dfoprab2  5966  cbvoprab2  5992  rexrnmpo  6035  opabex3d  6175  opabex3  6176  abexssex  6179  abexex  6180  oprabrexex2  6184  uchoice  6192  releldm2  6240  dfopab2  6244  dfoprab3s  6245  cnvoprab  6289  brtpos2  6306  tfr1onlemaccex  6403  tfrcllembxssdm  6411  tfrcllemaccex  6416  domen  6807  mapsnen  6867  xpsnen  6877  xpcomco  6882  xpassen  6886  fimax2gtri  6959  supelti  7063  cc1  7327  subhalfnqq  7476  ltbtwnnq  7478  prnmaxl  7550  prnminu  7551  prarloc  7565  genpdflem  7569  genpassl  7586  genpassu  7587  ltexprlemm  7662  2rexuz  9650  seq3f1olemp  10589  cbvsum  11506  cbvprod  11704  nnwosdc  12179  4sqlem12  12543  inffinp1  12589  ctiunctal  12601  unct  12602  isbasis2g  14224  tgval2  14230  ntreq0  14311  lmff  14428  metrest  14685  bj-axempty  15455  bj-axempty2  15456  bj-vprc  15458  bdinex1  15461  bj-zfpair2  15472  bj-uniex2  15478  bj-d0clsepcl  15487