Theorem exbii 1616

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

Syntax hints:   ↔ wb 105  ∃wex 1503

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 1458  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-4 1521  ax-ial 1545

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  2exbii  1617  3exbii  1618  exancom  1619  excom13  1700  exrot4  1702  eeor  1706  sbcof2  1821  sbequ8  1858  sbidm  1862  sborv  1902  19.41vv  1915  19.41vvv  1916  19.41vvvv  1917  exdistr  1921  19.42vvv  1924  exdistr2  1926  3exdistr  1927  4exdistr  1928  eean  1947  eeeanv  1949  ee4anv  1950  2sb5  1999  2sb5rf  2005  sbel2x  2014  sbexyz  2019  sbex  2020  exsb  2024  2exsb  2025  sb8eu  2055  sb8euh  2065  eu1  2067  eu2  2086  2moswapdc  2132  2exeu  2134  exists1  2138  clelab  2319  clabel  2320  sbabel  2363  rexbii2  2505  r2exf  2512  nfrexdya  2530  r19.41  2649  r19.43  2652  cbvreuvw  2732  isset  2766  rexv  2778  ceqsex2  2800  ceqsex3v  2802  gencbvex  2806  ceqsrexv  2890  rexab  2922  rexrab2  2927  euxfrdc  2946  euind  2947  reu6  2949  reu3  2950  2reuswapdc  2964  reuind  2965  sbccomlem  3060  rmo2ilem  3075  rexun  3339  reupick3  3444  abn0r  3471  abn0m  3472  rabn0m  3474  rexsns  3657  exsnrex  3660  snprc  3683  euabsn2  3687  reusn  3689  eusn  3692  elunirab  3848  unipr  3849  uniun  3854  uniin  3855  iuncom4  3919  dfiun2g  3944  iunn0m  3973  iunxiun  3994  disjnim  4020  cbvopab2  4103  cbvopab2v  4106  unopab  4108  zfnuleu  4153  0ex  4156  vnex  4160  inex1  4163  intexabim  4181  iinexgm  4183  inuni  4184  unidif0  4196  axpweq  4200  zfpow  4204  axpow2  4205  axpow3  4206  vpwex  4208  zfpair2  4239  mss  4255  exss  4256  opm  4263  eqvinop  4272  copsexg  4273  opabm  4311  iunopab  4312  zfun  4465  uniex2  4467  uniuni  4482  rexxfrd  4494  dtruex  4591  zfinf2  4621  elxp2  4677  opeliunxp  4714  xpiundi  4717  xpiundir  4718  elvvv  4722  eliunxp  4801  rexiunxp  4804  relop  4812  elco  4828  opelco2g  4830  cnvco  4847  cnvuni  4848  dfdm3  4849  dfrn2  4850  dfrn3  4851  elrng  4853  dfdm4  4854  eldm2g  4858  dmun  4869  dmin  4870  dmiun  4871  dmuni  4872  dmopab  4873  dmi  4877  dmmrnm  4881  elrn  4905  rnopab  4909  dmcosseq  4933  dmres  4963  elres  4978  elsnres  4979  dfima2  5007  elima3  5012  imadmrn  5015  imai  5021  args  5034  rniun  5076  ssrnres  5108  dmsnm  5131  dmsnopg  5137  elxp4  5153  elxp5  5154  cnvresima  5155  mptpreima  5159  dfco2  5165  coundi  5167  coundir  5168  resco  5170  imaco  5171  rnco  5172  coiun  5175  coi1  5181  coass  5184  xpcom  5212  dffun2  5264  imadif  5334  imainlem  5335  funimaexglem  5337  fun11iun  5521  f11o  5533  brprcneu  5547  nfvres  5588  fndmin  5665  abrexco  5802  imaiun  5803  dfoprab2  5965  cbvoprab2  5991  rexrnmpo  6034  opabex3d  6173  opabex3  6174  abexssex  6177  abexex  6178  oprabrexex2  6182  uchoice  6190  releldm2  6238  dfopab2  6242  dfoprab3s  6243  cnvoprab  6287  brtpos2  6304  tfr1onlemaccex  6401  tfrcllembxssdm  6409  tfrcllemaccex  6414  domen  6805  mapsnen  6865  xpsnen  6875  xpcomco  6880  xpassen  6884  fimax2gtri  6957  supelti  7061  cc1  7325  subhalfnqq  7474  ltbtwnnq  7476  prnmaxl  7548  prnminu  7549  prarloc  7563  genpdflem  7567  genpassl  7584  genpassu  7585  ltexprlemm  7660  2rexuz  9647  seq3f1olemp  10586  cbvsum  11503  cbvprod  11701  nnwosdc  12176  4sqlem12  12540  inffinp1  12586  ctiunctal  12598  unct  12599  isbasis2g  14213  tgval2  14219  ntreq0  14300  lmff  14417  metrest  14674  bj-axempty  15385  bj-axempty2  15386  bj-vprc  15388  bdinex1  15391  bj-zfpair2  15402  bj-uniex2  15408  bj-d0clsepcl  15417