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  1941  19.41vv  1955  19.41vvv  1956  19.41vvvv  1957  exdistr  1961  19.42vvv  1964  exdistr2  1966  3exdistr  1967  4exdistr  1968  eean  1987  eeeanv  1989  ee4anv  1990  2sb5  2039  2sb5rf  2045  sbel2x  2054  sbexyz  2059  sbex  2060  exsb  2064  2exsb  2065  sb8eu  2095  sb8euh  2105  eu1  2107  eu2  2127  2moswapdc  2173  2exeu  2175  exists1  2179  clelab  2362  clabel  2363  sbabel  2413  rexbii2  2555  r2exf  2562  nfrexdya  2580  r19.41  2700  r19.43  2703  cbvreuvw  2786  isset  2822  rexv  2834  ceqsex2  2857  ceqsex3v  2859  gencbvex  2863  ceqsrexv  2950  rexab  2982  rexrab2  2987  euxfrdc  3006  euind  3007  reu6  3009  reu3  3010  2reuswapdc  3024  reuind  3025  sbccomlem  3120  rmo2ilem  3136  rexun  3403  reupick3  3510  abn0r  3537  abn0m  3538  rabn0m  3540  rexsns  3733  exsnrex  3736  snprc  3759  euabsn2  3765  reusn  3767  eusn  3770  snmb  3818  elunirab  3932  unipr  3933  uniun  3938  uniin  3939  iuncom4  4003  dfiun2g  4028  iunn0m  4057  iunxiun  4078  disjnim  4104  cbvopab2  4189  cbvopab2v  4192  unopab  4194  zfnuleu  4239  0ex  4242  vnex  4246  inex1  4249  intexabim  4269  iinexgm  4271  inuni  4272  unidif0  4285  axpweq  4289  zfpow  4293  axpow2  4294  axpow3  4295  vpwex  4297  zfpair2  4328  mss  4347  exss  4348  opm  4355  eqvinop  4364  copsexg  4365  opabm  4404  iunopab  4405  zfun  4560  uniex2  4562  uniuni  4577  rexxfrd  4589  dtruex  4686  zfinf2  4716  elxp2  4772  opeliunxp  4810  xpiundi  4813  xpiundir  4814  elvvv  4818  eliunxp  4899  rexiunxp  4902  relop  4910  elco  4926  opelco2g  4928  cnvco  4945  cnvuni  4946  dfdm3  4947  dfrn2  4948  dfrn3  4949  elrng  4951  dfdm4  4953  eldm2g  4957  dmun  4968  dmin  4969  dmiun  4970  dmuni  4971  dmopab  4972  dmi  4976  reldmm  4980  dmmrnm  4981  elrn  5005  rnopab  5009  dmcosseq  5034  dmres  5064  elres  5079  elsnres  5080  dfima2  5108  elima3  5113  imadmrn  5116  imai  5123  args  5136  rniun  5178  ssrnres  5210  dmsnm  5233  dmsnopg  5239  elxp4  5255  elxp5  5256  cnvresima  5257  mptpreima  5261  dfco2  5267  coundi  5269  coundir  5270  resco  5272  imaco  5273  rnco  5274  coiun  5277  coi1  5283  coass  5286  xpcom  5314  dffun2  5367  imadif  5441  imainlem  5442  funimaexglem  5444  fun11iun  5640  f11o  5653  brprcneu  5668  nfvres  5711  fndmin  5790  abrexco  5938  imaiun  5939  dfoprab2  6108  cbvoprab2  6134  rexrnmpo  6177  opabex3d  6323  opabex3  6324  abexssex  6327  abexex  6328  oprabrexex2  6336  uchoice  6344  releldm2  6392  dfopab2  6396  dfoprab3s  6397  cnvoprab  6443  cnvimadfsn  6458  brtpos2  6495  tfr1onlemaccex  6592  tfrcllembxssdm  6600  tfrcllemaccex  6605  domen  7001  mapsnen  7066  xpsnen  7085  xpcomco  7090  xpassen  7094  fimax2gtri  7172  supelti  7306  cc1  7595  subhalfnqq  7745  ltbtwnnq  7747  prnmaxl  7819  prnminu  7820  prarloc  7834  genpdflem  7838  genpassl  7855  genpassu  7856  ltexprlemm  7931  2rexuz  9932  seq3f1olemp  10901  cbvsum  12070  cbvprod  12269  nnwosdc  12760  4sqlem12  13125  inffinp1  13264  ctiunctal  13276  unct  13277  isbasis2g  15036  tgval2  15042  ntreq0  15123  lmff  15240  metrest  15497  upgrex  16224  1loopgrvd2fi  16426  bj-axempty  16789  bj-axempty2  16790  bj-vprc  16792  bdinex1  16795  bj-zfpair2  16806  bj-uniex2  16812  bj-d0clsepcl  16821