Theorem exbii 1605

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

Syntax hints:   ↔ wb 105  ∃wex 1492

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 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510  ax-ial 1534

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  2exbii  1606  3exbii  1607  exancom  1608  excom13  1689  exrot4  1691  eeor  1695  sbcof2  1810  sbequ8  1847  sbidm  1851  sborv  1890  19.41vv  1903  19.41vvv  1904  19.41vvvv  1905  exdistr  1909  19.42vvv  1912  exdistr2  1914  3exdistr  1915  4exdistr  1916  eean  1931  eeeanv  1933  ee4anv  1934  2sb5  1983  2sb5rf  1989  sbel2x  1998  sbexyz  2003  sbex  2004  exsb  2008  2exsb  2009  sb8eu  2039  sb8euh  2049  eu1  2051  eu2  2070  2moswapdc  2116  2exeu  2118  exists1  2122  clelab  2303  clabel  2304  sbabel  2346  rexbii2  2488  r2exf  2495  nfrexdya  2513  r19.41  2632  r19.43  2635  cbvreuvw  2709  isset  2743  rexv  2755  ceqsex2  2777  ceqsex3v  2779  gencbvex  2783  ceqsrexv  2867  rexab  2899  rexrab2  2904  euxfrdc  2923  euind  2924  reu6  2926  reu3  2927  2reuswapdc  2941  reuind  2942  sbccomlem  3037  rmo2ilem  3052  rexun  3315  reupick3  3420  abn0r  3447  abn0m  3448  rabn0m  3450  rexsns  3631  exsnrex  3634  snprc  3657  euabsn2  3661  reusn  3663  eusn  3666  elunirab  3822  unipr  3823  uniun  3828  uniin  3829  iuncom4  3893  dfiun2g  3918  iunn0m  3947  iunxiun  3968  disjnim  3994  cbvopab2  4077  cbvopab2v  4080  unopab  4082  zfnuleu  4127  0ex  4130  vnex  4134  inex1  4137  intexabim  4152  iinexgm  4154  inuni  4155  unidif0  4167  axpweq  4171  zfpow  4175  axpow2  4176  axpow3  4177  vpwex  4179  zfpair2  4210  mss  4226  exss  4227  opm  4234  eqvinop  4243  copsexg  4244  opabm  4280  iunopab  4281  zfun  4434  uniex2  4436  uniuni  4451  rexxfrd  4463  dtruex  4558  zfinf2  4588  elxp2  4644  opeliunxp  4681  xpiundi  4684  xpiundir  4685  elvvv  4689  eliunxp  4766  rexiunxp  4769  relop  4777  elco  4793  opelco2g  4795  cnvco  4812  cnvuni  4813  dfdm3  4814  dfrn2  4815  dfrn3  4816  elrng  4818  dfdm4  4819  eldm2g  4823  dmun  4834  dmin  4835  dmiun  4836  dmuni  4837  dmopab  4838  dmi  4842  dmmrnm  4846  elrn  4870  rnopab  4874  dmcosseq  4898  dmres  4928  elres  4943  elsnres  4944  dfima2  4972  elima3  4977  imadmrn  4980  imai  4984  args  4997  rniun  5039  ssrnres  5071  dmsnm  5094  dmsnopg  5100  elxp4  5116  elxp5  5117  cnvresima  5118  mptpreima  5122  dfco2  5128  coundi  5130  coundir  5131  resco  5133  imaco  5134  rnco  5135  coiun  5138  coi1  5144  coass  5147  xpcom  5175  dffun2  5226  imadif  5296  imainlem  5297  funimaexglem  5299  fun11iun  5482  f11o  5494  brprcneu  5508  nfvres  5548  fndmin  5623  abrexco  5759  imaiun  5760  dfoprab2  5921  cbvoprab2  5947  rexrnmpo  5989  opabex3d  6121  opabex3  6122  abexssex  6125  abexex  6126  oprabrexex2  6130  releldm2  6185  dfopab2  6189  dfoprab3s  6190  cnvoprab  6234  brtpos2  6251  tfr1onlemaccex  6348  tfrcllembxssdm  6356  tfrcllemaccex  6361  domen  6750  mapsnen  6810  xpsnen  6820  xpcomco  6825  xpassen  6829  fimax2gtri  6900  supelti  7000  cc1  7263  subhalfnqq  7412  ltbtwnnq  7414  prnmaxl  7486  prnminu  7487  prarloc  7501  genpdflem  7505  genpassl  7522  genpassu  7523  ltexprlemm  7598  2rexuz  9581  seq3f1olemp  10501  cbvsum  11367  cbvprod  11565  nnwosdc  12039  inffinp1  12429  ctiunctal  12441  unct  12442  isbasis2g  13515  tgval2  13521  ntreq0  13602  lmff  13719  metrest  13976  bj-axempty  14615  bj-axempty2  14616  bj-vprc  14618  bdinex1  14621  bj-zfpair2  14632  bj-uniex2  14638  bj-d0clsepcl  14647