Theorem exbii 1536

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

Syntax hints:   ↔ wb 103  ∃wex 1421

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 1376  ax-gen 1378  ax-ie1 1422  ax-ie2 1423  ax-4 1440  ax-ial 1467

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  2exbii  1537  3exbii  1538  exancom  1539  excom13  1619  exrot4  1621  eeor  1625  sbcof2  1731  sbequ8  1768  sbidm  1772  sborv  1811  19.41vv  1824  19.41vvv  1825  19.41vvvv  1826  exdistr  1828  19.42vvv  1830  exdistr2  1832  3exdistr  1833  4exdistr  1834  eean  1847  eeeanv  1849  ee4anv  1850  2sb5  1900  2sb5rf  1906  sbel2x  1915  sbexyz  1920  sbex  1921  exsb  1925  2exsb  1926  sb8eu  1954  sb8euh  1964  eu1  1966  eu2  1985  2moswapdc  2031  2exeu  2033  exists1  2037  clelab  2203  clabel  2204  sbabel  2244  rexbii2  2377  r2exf  2384  nfrexdya  2401  r19.41  2509  r19.43  2512  isset  2605  rexv  2617  ceqsex2  2639  ceqsex3v  2641  gencbvex  2645  ceqsrexv  2725  rexab  2754  rexrab2  2759  euxfrdc  2778  euind  2779  reu6  2781  reu3  2782  2reuswapdc  2794  reuind  2795  sbccomlem  2888  rmo2ilem  2903  rexun  3152  reupick3  3249  abn0r  3270  rabn0m  3272  rexsns  3432  exsnrex  3435  snprc  3457  euabsn2  3461  reusn  3463  eusn  3466  elunirab  3614  unipr  3615  uniun  3620  uniin  3621  iuncom4  3685  dfiun2g  3710  iunn0m  3738  iunxiun  3757  cbvopab2  3852  cbvopab2v  3855  unopab  3857  zfnuleu  3902  0ex  3905  vprc  3909  inex1  3912  intexabim  3927  iinexgm  3929  inuni  3930  unidif0  3941  axpweq  3945  zfpow  3949  axpow2  3950  axpow3  3951  pwex  3953  zfpair2  3965  mss  3981  exss  3982  opm  3989  eqvinop  3998  copsexg  3999  opabm  4035  iunopab  4036  zfun  4189  uniex2  4191  uniuni  4201  rexxfrd  4213  dtruex  4302  zfinf2  4330  elxp2  4381  opeliunxp  4413  xpiundi  4416  xpiundir  4417  elvvv  4421  eliunxp  4493  rexiunxp  4496  relop  4504  opelco2g  4521  cnvco  4538  cnvuni  4539  dfdm3  4540  dfrn2  4541  dfrn3  4542  elrng  4544  dfdm4  4545  eldm2g  4549  dmun  4560  dmin  4561  dmiun  4562  dmuni  4563  dmopab  4564  dmi  4568  dmmrnm  4572  elrn  4595  rnopab  4599  dmcosseq  4621  dmres  4650  elres  4664  elsnres  4665  dfima2  4690  elima3  4695  imadmrn  4698  imai  4701  args  4714  rniun  4754  ssrnres  4783  dmsnm  4806  dmsnopg  4812  elxp4  4828  elxp5  4829  cnvresima  4830  mptpreima  4834  dfco2  4840  coundi  4842  coundir  4843  resco  4845  imaco  4846  rnco  4847  coiun  4850  coi1  4856  coass  4859  xpcom  4884  dffun2  4932  imadif  4999  imainlem  5000  funimaexglem  5002  fun11iun  5167  f11o  5179  brprcneu  5191  nfvres  5227  fndmin  5295  abrexco  5419  imaiun  5420  dfoprab2  5572  cbvoprab2  5597  rexrnmpt2  5636  opabex3d  5768  opabex3  5769  abexssex  5772  abexex  5773  oprabrexex2  5777  releldm2  5831  dfopab2  5835  dfoprab3s  5836  cnvoprab  5875  brtpos2  5889  domen  6255  xpsnen  6318  xpcomco  6323  xpassen  6327  supelti  6415  subhalfnqq  6604  ltbtwnnq  6606  prnmaxl  6678  prnminu  6679  prarloc  6693  genpdflem  6697  genpassl  6714  genpassu  6715  ltexprlemm  6790  2rexuz  8670  bj-axempty  10684  bj-axempty2  10685  bj-vprc  10687  bdinex1  10690  bj-zfpair2  10701  bj-uniex2  10707  bj-d0clsepcl  10720