Theorem exbii 1654

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

Syntax hints:   ↔ wb 105  ∃wex 1541

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 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-ial 1583

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  2exbii  1655  3exbii  1656  exancom  1657  excom13  1737  exrot4  1739  eeor  1743  sbcof2  1859  sbequ8  1896  sbidm  1900  sborv  1940  19.41vv  1953  19.41vvv  1954  19.41vvvv  1955  exdistr  1959  19.42vvv  1962  exdistr2  1964  3exdistr  1965  4exdistr  1966  eean  1985  eeeanv  1987  ee4anv  1988  2sb5  2037  2sb5rf  2043  sbel2x  2052  sbexyz  2057  sbex  2058  exsb  2062  2exsb  2063  sb8eu  2093  sb8euh  2103  eu1  2105  eu2  2125  2moswapdc  2171  2exeu  2173  exists1  2177  clelab  2360  clabel  2361  sbabel  2411  rexbii2  2553  r2exf  2560  nfrexdya  2578  r19.41  2698  r19.43  2701  cbvreuvw  2784  isset  2820  rexv  2832  ceqsex2  2855  ceqsex3v  2857  gencbvex  2861  ceqsrexv  2947  rexab  2979  rexrab2  2984  euxfrdc  3003  euind  3004  reu6  3006  reu3  3007  2reuswapdc  3021  reuind  3022  sbccomlem  3117  rmo2ilem  3133  rexun  3399  reupick3  3506  abn0r  3533  abn0m  3534  rabn0m  3536  rexsns  3728  exsnrex  3731  snprc  3754  euabsn2  3760  reusn  3762  eusn  3765  snmb  3813  elunirab  3927  unipr  3928  uniun  3933  uniin  3934  iuncom4  3998  dfiun2g  4023  iunn0m  4052  iunxiun  4073  disjnim  4099  cbvopab2  4184  cbvopab2v  4187  unopab  4189  zfnuleu  4234  0ex  4237  vnex  4241  inex1  4244  intexabim  4264  iinexgm  4266  inuni  4267  unidif0  4280  axpweq  4284  zfpow  4288  axpow2  4289  axpow3  4290  vpwex  4292  zfpair2  4323  mss  4342  exss  4343  opm  4350  eqvinop  4359  copsexg  4360  opabm  4399  iunopab  4400  zfun  4555  uniex2  4557  uniuni  4572  rexxfrd  4584  dtruex  4681  zfinf2  4711  elxp2  4767  opeliunxp  4805  xpiundi  4808  xpiundir  4809  elvvv  4813  eliunxp  4894  rexiunxp  4897  relop  4905  elco  4921  opelco2g  4923  cnvco  4940  cnvuni  4941  dfdm3  4942  dfrn2  4943  dfrn3  4944  elrng  4946  dfdm4  4948  eldm2g  4952  dmun  4963  dmin  4964  dmiun  4965  dmuni  4966  dmopab  4967  dmi  4971  reldmm  4975  dmmrnm  4976  elrn  5000  rnopab  5004  dmcosseq  5029  dmres  5059  elres  5074  elsnres  5075  dfima2  5103  elima3  5108  imadmrn  5111  imai  5118  args  5131  rniun  5173  ssrnres  5205  dmsnm  5228  dmsnopg  5234  elxp4  5250  elxp5  5251  cnvresima  5252  mptpreima  5256  dfco2  5262  coundi  5264  coundir  5265  resco  5267  imaco  5268  rnco  5269  coiun  5272  coi1  5278  coass  5281  xpcom  5309  dffun2  5362  imadif  5436  imainlem  5437  funimaexglem  5439  fun11iun  5635  f11o  5648  brprcneu  5663  nfvres  5706  fndmin  5785  abrexco  5932  imaiun  5933  dfoprab2  6100  cbvoprab2  6126  rexrnmpo  6169  opabex3d  6314  opabex3  6315  abexssex  6318  abexex  6319  oprabrexex2  6323  uchoice  6331  releldm2  6379  dfopab2  6383  dfoprab3s  6384  cnvoprab  6430  cnvimadfsn  6445  brtpos2  6482  tfr1onlemaccex  6579  tfrcllembxssdm  6587  tfrcllemaccex  6592  domen  6988  mapsnen  7053  xpsnen  7072  xpcomco  7077  xpassen  7081  fimax2gtri  7159  supelti  7293  cc1  7579  subhalfnqq  7729  ltbtwnnq  7731  prnmaxl  7803  prnminu  7804  prarloc  7818  genpdflem  7822  genpassl  7839  genpassu  7840  ltexprlemm  7915  2rexuz  9914  seq3f1olemp  10877  cbvsum  12045  cbvprod  12244  nnwosdc  12735  4sqlem12  13100  inffinp1  13180  ctiunctal  13192  unct  13193  isbasis2g  14910  tgval2  14916  ntreq0  14997  lmff  15114  metrest  15371  upgrex  16098  1loopgrvd2fi  16300  bj-axempty  16663  bj-axempty2  16664  bj-vprc  16666  bdinex1  16669  bj-zfpair2  16680  bj-uniex2  16686  bj-d0clsepcl  16695