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  2710  isset  2744  rexv  2756  ceqsex2  2778  ceqsex3v  2780  gencbvex  2784  ceqsrexv  2868  rexab  2900  rexrab2  2905  euxfrdc  2924  euind  2925  reu6  2927  reu3  2928  2reuswapdc  2942  reuind  2943  sbccomlem  3038  rmo2ilem  3053  rexun  3316  reupick3  3421  abn0r  3448  abn0m  3449  rabn0m  3451  rexsns  3632  exsnrex  3635  snprc  3658  euabsn2  3662  reusn  3664  eusn  3667  elunirab  3823  unipr  3824  uniun  3829  uniin  3830  iuncom4  3894  dfiun2g  3919  iunn0m  3948  iunxiun  3969  disjnim  3995  cbvopab2  4078  cbvopab2v  4081  unopab  4083  zfnuleu  4128  0ex  4131  vnex  4135  inex1  4138  intexabim  4153  iinexgm  4155  inuni  4156  unidif0  4168  axpweq  4172  zfpow  4176  axpow2  4177  axpow3  4178  vpwex  4180  zfpair2  4211  mss  4227  exss  4228  opm  4235  eqvinop  4244  copsexg  4245  opabm  4281  iunopab  4282  zfun  4435  uniex2  4437  uniuni  4452  rexxfrd  4464  dtruex  4559  zfinf2  4589  elxp2  4645  opeliunxp  4682  xpiundi  4685  xpiundir  4686  elvvv  4690  eliunxp  4767  rexiunxp  4770  relop  4778  elco  4794  opelco2g  4796  cnvco  4813  cnvuni  4814  dfdm3  4815  dfrn2  4816  dfrn3  4817  elrng  4819  dfdm4  4820  eldm2g  4824  dmun  4835  dmin  4836  dmiun  4837  dmuni  4838  dmopab  4839  dmi  4843  dmmrnm  4847  elrn  4871  rnopab  4875  dmcosseq  4899  dmres  4929  elres  4944  elsnres  4945  dfima2  4973  elima3  4978  imadmrn  4981  imai  4985  args  4998  rniun  5040  ssrnres  5072  dmsnm  5095  dmsnopg  5101  elxp4  5117  elxp5  5118  cnvresima  5119  mptpreima  5123  dfco2  5129  coundi  5131  coundir  5132  resco  5134  imaco  5135  rnco  5136  coiun  5139  coi1  5145  coass  5148  xpcom  5176  dffun2  5227  imadif  5297  imainlem  5298  funimaexglem  5300  fun11iun  5483  f11o  5495  brprcneu  5509  nfvres  5549  fndmin  5624  abrexco  5760  imaiun  5761  dfoprab2  5922  cbvoprab2  5948  rexrnmpo  5990  opabex3d  6122  opabex3  6123  abexssex  6126  abexex  6127  oprabrexex2  6131  releldm2  6186  dfopab2  6190  dfoprab3s  6191  cnvoprab  6235  brtpos2  6252  tfr1onlemaccex  6349  tfrcllembxssdm  6357  tfrcllemaccex  6362  domen  6751  mapsnen  6811  xpsnen  6821  xpcomco  6826  xpassen  6830  fimax2gtri  6901  supelti  7001  cc1  7264  subhalfnqq  7413  ltbtwnnq  7415  prnmaxl  7487  prnminu  7488  prarloc  7502  genpdflem  7506  genpassl  7523  genpassu  7524  ltexprlemm  7599  2rexuz  9582  seq3f1olemp  10502  cbvsum  11368  cbvprod  11566  nnwosdc  12040  inffinp1  12430  ctiunctal  12442  unct  12443  isbasis2g  13548  tgval2  13554  ntreq0  13635  lmff  13752  metrest  14009  bj-axempty  14648  bj-axempty2  14649  bj-vprc  14651  bdinex1  14654  bj-zfpair2  14665  bj-uniex2  14671  bj-d0clsepcl  14680