Theorem exbii 1651

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

Syntax hints:   ↔ wb 105  ∃wex 1538

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 1493  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-4 1556  ax-ial 1580

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  2exbii  1652  3exbii  1653  exancom  1654  excom13  1735  exrot4  1737  eeor  1741  sbcof2  1856  sbequ8  1893  sbidm  1897  sborv  1937  19.41vv  1950  19.41vvv  1951  19.41vvvv  1952  exdistr  1956  19.42vvv  1959  exdistr2  1961  3exdistr  1962  4exdistr  1963  eean  1982  eeeanv  1984  ee4anv  1985  2sb5  2034  2sb5rf  2040  sbel2x  2049  sbexyz  2054  sbex  2055  exsb  2059  2exsb  2060  sb8eu  2090  sb8euh  2100  eu1  2102  eu2  2122  2moswapdc  2168  2exeu  2170  exists1  2174  clelab  2355  clabel  2356  sbabel  2399  rexbii2  2541  r2exf  2548  nfrexdya  2566  r19.41  2686  r19.43  2689  cbvreuvw  2771  isset  2807  rexv  2819  ceqsex2  2842  ceqsex3v  2844  gencbvex  2848  ceqsrexv  2934  rexab  2966  rexrab2  2971  euxfrdc  2990  euind  2991  reu6  2993  reu3  2994  2reuswapdc  3008  reuind  3009  sbccomlem  3104  rmo2ilem  3120  rexun  3385  reupick3  3490  abn0r  3517  abn0m  3518  rabn0m  3520  rexsns  3706  exsnrex  3709  snprc  3732  euabsn2  3738  reusn  3740  eusn  3743  snmb  3791  elunirab  3904  unipr  3905  uniun  3910  uniin  3911  iuncom4  3975  dfiun2g  4000  iunn0m  4029  iunxiun  4050  disjnim  4076  cbvopab2  4161  cbvopab2v  4164  unopab  4166  zfnuleu  4211  0ex  4214  vnex  4218  inex1  4221  intexabim  4240  iinexgm  4242  inuni  4243  unidif0  4255  axpweq  4259  zfpow  4263  axpow2  4264  axpow3  4265  vpwex  4267  zfpair2  4298  mss  4316  exss  4317  opm  4324  eqvinop  4333  copsexg  4334  opabm  4373  iunopab  4374  zfun  4529  uniex2  4531  uniuni  4546  rexxfrd  4558  dtruex  4655  zfinf2  4685  elxp2  4741  opeliunxp  4779  xpiundi  4782  xpiundir  4783  elvvv  4787  eliunxp  4867  rexiunxp  4870  relop  4878  elco  4894  opelco2g  4896  cnvco  4913  cnvuni  4914  dfdm3  4915  dfrn2  4916  dfrn3  4917  elrng  4919  dfdm4  4921  eldm2g  4925  dmun  4936  dmin  4937  dmiun  4938  dmuni  4939  dmopab  4940  dmi  4944  reldmm  4948  dmmrnm  4949  elrn  4973  rnopab  4977  dmcosseq  5002  dmres  5032  elres  5047  elsnres  5048  dfima2  5076  elima3  5081  imadmrn  5084  imai  5090  args  5103  rniun  5145  ssrnres  5177  dmsnm  5200  dmsnopg  5206  elxp4  5222  elxp5  5223  cnvresima  5224  mptpreima  5228  dfco2  5234  coundi  5236  coundir  5237  resco  5239  imaco  5240  rnco  5241  coiun  5244  coi1  5250  coass  5253  xpcom  5281  dffun2  5334  imadif  5407  imainlem  5408  funimaexglem  5410  fun11iun  5601  f11o  5613  brprcneu  5628  nfvres  5671  fndmin  5750  abrexco  5895  imaiun  5896  dfoprab2  6063  cbvoprab2  6089  rexrnmpo  6132  opabex3d  6278  opabex3  6279  abexssex  6282  abexex  6283  oprabrexex2  6287  uchoice  6295  releldm2  6343  dfopab2  6347  dfoprab3s  6348  cnvoprab  6394  brtpos2  6412  tfr1onlemaccex  6509  tfrcllembxssdm  6517  tfrcllemaccex  6522  domen  6917  mapsnen  6981  xpsnen  7000  xpcomco  7005  xpassen  7009  fimax2gtri  7084  supelti  7192  cc1  7474  subhalfnqq  7624  ltbtwnnq  7626  prnmaxl  7698  prnminu  7699  prarloc  7713  genpdflem  7717  genpassl  7734  genpassu  7735  ltexprlemm  7810  2rexuz  9806  seq3f1olemp  10767  cbvsum  11911  cbvprod  12109  nnwosdc  12600  4sqlem12  12965  inffinp1  13040  ctiunctal  13052  unct  13053  isbasis2g  14759  tgval2  14765  ntreq0  14846  lmff  14963  metrest  15220  upgrex  15944  1loopgrvd2fi  16111  bj-axempty  16424  bj-axempty2  16425  bj-vprc  16427  bdinex1  16430  bj-zfpair2  16441  bj-uniex2  16447  bj-d0clsepcl  16456