Theorem exbii 1539

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

Syntax hints:   ↔ wb 103  ∃wex 1424

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1379  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-4 1443  ax-ial 1470

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  2exbii  1540  3exbii  1541  exancom  1542  excom13  1622  exrot4  1624  eeor  1628  sbcof2  1735  sbequ8  1772  sbidm  1776  sborv  1815  19.41vv  1828  19.41vvv  1829  19.41vvvv  1830  exdistr  1832  19.42vvv  1834  exdistr2  1836  3exdistr  1837  4exdistr  1838  eean  1851  eeeanv  1853  ee4anv  1854  2sb5  1904  2sb5rf  1910  sbel2x  1919  sbexyz  1924  sbex  1925  exsb  1929  2exsb  1930  sb8eu  1958  sb8euh  1968  eu1  1970  eu2  1989  2moswapdc  2035  2exeu  2037  exists1  2041  clelab  2209  clabel  2210  sbabel  2250  rexbii2  2385  r2exf  2392  nfrexdya  2409  r19.41  2518  r19.43  2521  isset  2619  rexv  2631  ceqsex2  2653  ceqsex3v  2655  gencbvex  2659  ceqsrexv  2738  rexab  2768  rexrab2  2773  euxfrdc  2792  euind  2793  reu6  2795  reu3  2796  2reuswapdc  2808  reuind  2809  sbccomlem  2902  rmo2ilem  2917  rexun  3169  reupick3  3273  abn0r  3296  abn0m  3297  rabn0m  3299  rexsns  3465  exsnrex  3468  snprc  3490  euabsn2  3494  reusn  3496  eusn  3499  elunirab  3649  unipr  3650  uniun  3655  uniin  3656  iuncom4  3720  dfiun2g  3745  iunn0m  3773  iunxiun  3792  cbvopab2  3887  cbvopab2v  3890  unopab  3892  zfnuleu  3937  0ex  3940  vnex  3944  inex1  3947  intexabim  3962  iinexgm  3964  inuni  3965  unidif0  3976  axpweq  3980  zfpow  3984  axpow2  3985  axpow3  3986  vpwex  3988  zfpair2  4010  mss  4026  exss  4027  opm  4034  eqvinop  4043  copsexg  4044  opabm  4080  iunopab  4081  zfun  4234  uniex2  4236  uniuni  4246  rexxfrd  4258  dtruex  4347  zfinf2  4376  elxp2  4428  opeliunxp  4460  xpiundi  4463  xpiundir  4464  elvvv  4468  eliunxp  4542  rexiunxp  4545  relop  4553  elco  4569  opelco2g  4571  cnvco  4588  cnvuni  4589  dfdm3  4590  dfrn2  4591  dfrn3  4592  elrng  4594  dfdm4  4595  eldm2g  4599  dmun  4610  dmin  4611  dmiun  4612  dmuni  4613  dmopab  4614  dmi  4618  dmmrnm  4622  elrn  4645  rnopab  4649  dmcosseq  4671  dmres  4700  elres  4714  elsnres  4715  dfima2  4740  elima3  4745  imadmrn  4748  imai  4752  args  4765  rniun  4805  ssrnres  4836  dmsnm  4859  dmsnopg  4865  elxp4  4881  elxp5  4882  cnvresima  4883  mptpreima  4887  dfco2  4893  coundi  4895  coundir  4896  resco  4898  imaco  4899  rnco  4900  coiun  4903  coi1  4909  coass  4912  xpcom  4940  dffun2  4988  imadif  5056  imainlem  5057  funimaexglem  5059  fun11iun  5231  f11o  5243  brprcneu  5255  nfvres  5294  fndmin  5363  abrexco  5493  imaiun  5494  dfoprab2  5647  cbvoprab2  5672  rexrnmpt2  5711  opabex3d  5843  opabex3  5844  abexssex  5847  abexex  5848  oprabrexex2  5852  releldm2  5906  dfopab2  5910  dfoprab3s  5911  cnvoprab  5950  brtpos2  5964  tfr1onlemaccex  6061  tfrcllembxssdm  6069  tfrcllemaccex  6074  domen  6414  mapsnen  6474  xpsnen  6483  xpcomco  6488  xpassen  6492  fimax2gtri  6563  supelti  6634  subhalfnqq  6910  ltbtwnnq  6912  prnmaxl  6984  prnminu  6985  prarloc  6999  genpdflem  7003  genpassl  7020  genpassu  7021  ltexprlemm  7096  2rexuz  8995  iseqf1olemp  9828  cbvsum  10632  bj-axempty  11214  bj-axempty2  11215  bj-vprc  11217  bdinex1  11220  bj-zfpair2  11231  bj-uniex2  11237  bj-d0clsepcl  11250