Theorem exbii 1592

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

Syntax hints:   ↔ wb 104  ∃wex 1479

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1434  ax-gen 1436  ax-ie1 1480  ax-ie2 1481  ax-4 1497  ax-ial 1521

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  2exbii  1593  3exbii  1594  exancom  1595  excom13  1676  exrot4  1678  eeor  1682  sbcof2  1797  sbequ8  1834  sbidm  1838  sborv  1877  19.41vv  1890  19.41vvv  1891  19.41vvvv  1892  exdistr  1896  19.42vvv  1899  exdistr2  1901  3exdistr  1902  4exdistr  1903  eean  1918  eeeanv  1920  ee4anv  1921  2sb5  1970  2sb5rf  1976  sbel2x  1985  sbexyz  1990  sbex  1991  exsb  1995  2exsb  1996  sb8eu  2026  sb8euh  2036  eu1  2038  eu2  2057  2moswapdc  2103  2exeu  2105  exists1  2109  clelab  2290  clabel  2291  sbabel  2333  rexbii2  2475  r2exf  2482  nfrexdya  2500  r19.41  2619  r19.43  2622  cbvreuvw  2695  isset  2727  rexv  2739  ceqsex2  2761  ceqsex3v  2763  gencbvex  2767  ceqsrexv  2851  rexab  2883  rexrab2  2888  euxfrdc  2907  euind  2908  reu6  2910  reu3  2911  2reuswapdc  2925  reuind  2926  sbccomlem  3020  rmo2ilem  3035  rexun  3297  reupick3  3402  abn0r  3428  abn0m  3429  rabn0m  3431  rexsns  3609  exsnrex  3612  snprc  3635  euabsn2  3639  reusn  3641  eusn  3644  elunirab  3796  unipr  3797  uniun  3802  uniin  3803  iuncom4  3867  dfiun2g  3892  iunn0m  3920  iunxiun  3941  disjnim  3967  cbvopab2  4050  cbvopab2v  4053  unopab  4055  zfnuleu  4100  0ex  4103  vnex  4107  inex1  4110  intexabim  4125  iinexgm  4127  inuni  4128  unidif0  4140  axpweq  4144  zfpow  4148  axpow2  4149  axpow3  4150  vpwex  4152  zfpair2  4182  mss  4198  exss  4199  opm  4206  eqvinop  4215  copsexg  4216  opabm  4252  iunopab  4253  zfun  4406  uniex2  4408  uniuni  4423  rexxfrd  4435  dtruex  4530  zfinf2  4560  elxp2  4616  opeliunxp  4653  xpiundi  4656  xpiundir  4657  elvvv  4661  eliunxp  4737  rexiunxp  4740  relop  4748  elco  4764  opelco2g  4766  cnvco  4783  cnvuni  4784  dfdm3  4785  dfrn2  4786  dfrn3  4787  elrng  4789  dfdm4  4790  eldm2g  4794  dmun  4805  dmin  4806  dmiun  4807  dmuni  4808  dmopab  4809  dmi  4813  dmmrnm  4817  elrn  4841  rnopab  4845  dmcosseq  4869  dmres  4899  elres  4914  elsnres  4915  dfima2  4942  elima3  4947  imadmrn  4950  imai  4954  args  4967  rniun  5008  ssrnres  5040  dmsnm  5063  dmsnopg  5069  elxp4  5085  elxp5  5086  cnvresima  5087  mptpreima  5091  dfco2  5097  coundi  5099  coundir  5100  resco  5102  imaco  5103  rnco  5104  coiun  5107  coi1  5113  coass  5116  xpcom  5144  dffun2  5192  imadif  5262  imainlem  5263  funimaexglem  5265  fun11iun  5447  f11o  5459  brprcneu  5473  nfvres  5513  fndmin  5586  abrexco  5721  imaiun  5722  dfoprab2  5880  cbvoprab2  5906  rexrnmpo  5948  opabex3d  6081  opabex3  6082  abexssex  6085  abexex  6086  oprabrexex2  6090  releldm2  6145  dfopab2  6149  dfoprab3s  6150  cnvoprab  6193  brtpos2  6210  tfr1onlemaccex  6307  tfrcllembxssdm  6315  tfrcllemaccex  6320  domen  6708  mapsnen  6768  xpsnen  6778  xpcomco  6783  xpassen  6787  fimax2gtri  6858  supelti  6958  cc1  7197  subhalfnqq  7346  ltbtwnnq  7348  prnmaxl  7420  prnminu  7421  prarloc  7435  genpdflem  7439  genpassl  7456  genpassu  7457  ltexprlemm  7532  2rexuz  9511  seq3f1olemp  10427  cbvsum  11287  cbvprod  11485  inffinp1  12299  ctiunctal  12311  unct  12312  isbasis2g  12584  tgval2  12592  ntreq0  12673  lmff  12790  metrest  13047  bj-axempty  13610  bj-axempty2  13611  bj-vprc  13613  bdinex1  13616  bj-zfpair2  13627  bj-uniex2  13633  bj-d0clsepcl  13642