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  2806  rexv  2818  ceqsex2  2841  ceqsex3v  2843  gencbvex  2847  ceqsrexv  2933  rexab  2965  rexrab2  2970  euxfrdc  2989  euind  2990  reu6  2992  reu3  2993  2reuswapdc  3007  reuind  3008  sbccomlem  3103  rmo2ilem  3119  rexun  3384  reupick3  3489  abn0r  3516  abn0m  3517  rabn0m  3519  rexsns  3705  exsnrex  3708  snprc  3731  euabsn2  3735  reusn  3737  eusn  3740  snmb  3787  elunirab  3900  unipr  3901  uniun  3906  uniin  3907  iuncom4  3971  dfiun2g  3996  iunn0m  4025  iunxiun  4046  disjnim  4072  cbvopab2  4157  cbvopab2v  4160  unopab  4162  zfnuleu  4207  0ex  4210  vnex  4214  inex1  4217  intexabim  4235  iinexgm  4237  inuni  4238  unidif0  4250  axpweq  4254  zfpow  4258  axpow2  4259  axpow3  4260  vpwex  4262  zfpair2  4293  mss  4311  exss  4312  opm  4319  eqvinop  4328  copsexg  4329  opabm  4368  iunopab  4369  zfun  4524  uniex2  4526  uniuni  4541  rexxfrd  4553  dtruex  4650  zfinf2  4680  elxp2  4736  opeliunxp  4773  xpiundi  4776  xpiundir  4777  elvvv  4781  eliunxp  4860  rexiunxp  4863  relop  4871  elco  4887  opelco2g  4889  cnvco  4906  cnvuni  4907  dfdm3  4908  dfrn2  4909  dfrn3  4910  elrng  4912  dfdm4  4914  eldm2g  4918  dmun  4929  dmin  4930  dmiun  4931  dmuni  4932  dmopab  4933  dmi  4937  reldmm  4941  dmmrnm  4942  elrn  4966  rnopab  4970  dmcosseq  4995  dmres  5025  elres  5040  elsnres  5041  dfima2  5069  elima3  5074  imadmrn  5077  imai  5083  args  5096  rniun  5138  ssrnres  5170  dmsnm  5193  dmsnopg  5199  elxp4  5215  elxp5  5216  cnvresima  5217  mptpreima  5221  dfco2  5227  coundi  5229  coundir  5230  resco  5232  imaco  5233  rnco  5234  coiun  5237  coi1  5243  coass  5246  xpcom  5274  dffun2  5327  imadif  5400  imainlem  5401  funimaexglem  5403  fun11iun  5592  f11o  5604  brprcneu  5619  nfvres  5662  fndmin  5741  abrexco  5882  imaiun  5883  dfoprab2  6050  cbvoprab2  6076  rexrnmpo  6119  opabex3d  6264  opabex3  6265  abexssex  6268  abexex  6269  oprabrexex2  6273  uchoice  6281  releldm2  6329  dfopab2  6333  dfoprab3s  6334  cnvoprab  6378  brtpos2  6395  tfr1onlemaccex  6492  tfrcllembxssdm  6500  tfrcllemaccex  6505  domen  6898  mapsnen  6962  xpsnen  6976  xpcomco  6981  xpassen  6985  fimax2gtri  7059  supelti  7165  cc1  7447  subhalfnqq  7597  ltbtwnnq  7599  prnmaxl  7671  prnminu  7672  prarloc  7686  genpdflem  7690  genpassl  7707  genpassu  7708  ltexprlemm  7783  2rexuz  9773  seq3f1olemp  10732  cbvsum  11866  cbvprod  12064  nnwosdc  12555  4sqlem12  12920  inffinp1  12995  ctiunctal  13007  unct  13008  isbasis2g  14713  tgval2  14719  ntreq0  14800  lmff  14917  metrest  15174  upgrex  15897  bj-axempty  16214  bj-axempty2  16215  bj-vprc  16217  bdinex1  16220  bj-zfpair2  16231  bj-uniex2  16237  bj-d0clsepcl  16246