Theorem exbii 1584

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

Syntax hints:   ↔ wb 104  ∃wex 1468

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 1423  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-4 1487  ax-ial 1514

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  2exbii  1585  3exbii  1586  exancom  1587  excom13  1667  exrot4  1669  eeor  1673  sbcof2  1782  sbequ8  1819  sbidm  1823  sborv  1862  19.41vv  1875  19.41vvv  1876  19.41vvvv  1877  exdistr  1881  19.42vvv  1884  exdistr2  1886  3exdistr  1887  4exdistr  1888  eean  1903  eeeanv  1905  ee4anv  1906  2sb5  1958  2sb5rf  1964  sbel2x  1973  sbexyz  1978  sbex  1979  exsb  1983  2exsb  1984  sb8eu  2012  sb8euh  2022  eu1  2024  eu2  2043  2moswapdc  2089  2exeu  2091  exists1  2095  clelab  2265  clabel  2266  sbabel  2307  rexbii2  2446  r2exf  2453  nfrexdya  2470  r19.41  2586  r19.43  2589  isset  2692  rexv  2704  ceqsex2  2726  ceqsex3v  2728  gencbvex  2732  ceqsrexv  2815  rexab  2846  rexrab2  2851  euxfrdc  2870  euind  2871  reu6  2873  reu3  2874  2reuswapdc  2888  reuind  2889  sbccomlem  2983  rmo2ilem  2998  rexun  3256  reupick3  3361  abn0r  3387  abn0m  3388  rabn0m  3390  rexsns  3563  exsnrex  3566  snprc  3588  euabsn2  3592  reusn  3594  eusn  3597  elunirab  3749  unipr  3750  uniun  3755  uniin  3756  iuncom4  3820  dfiun2g  3845  iunn0m  3873  iunxiun  3894  disjnim  3920  cbvopab2  4002  cbvopab2v  4005  unopab  4007  zfnuleu  4052  0ex  4055  vnex  4059  inex1  4062  intexabim  4077  iinexgm  4079  inuni  4080  unidif0  4091  axpweq  4095  zfpow  4099  axpow2  4100  axpow3  4101  vpwex  4103  zfpair2  4132  mss  4148  exss  4149  opm  4156  eqvinop  4165  copsexg  4166  opabm  4202  iunopab  4203  zfun  4356  uniex2  4358  uniuni  4372  rexxfrd  4384  dtruex  4474  zfinf2  4503  elxp2  4557  opeliunxp  4594  xpiundi  4597  xpiundir  4598  elvvv  4602  eliunxp  4678  rexiunxp  4681  relop  4689  elco  4705  opelco2g  4707  cnvco  4724  cnvuni  4725  dfdm3  4726  dfrn2  4727  dfrn3  4728  elrng  4730  dfdm4  4731  eldm2g  4735  dmun  4746  dmin  4747  dmiun  4748  dmuni  4749  dmopab  4750  dmi  4754  dmmrnm  4758  elrn  4782  rnopab  4786  dmcosseq  4810  dmres  4840  elres  4855  elsnres  4856  dfima2  4883  elima3  4888  imadmrn  4891  imai  4895  args  4908  rniun  4949  ssrnres  4981  dmsnm  5004  dmsnopg  5010  elxp4  5026  elxp5  5027  cnvresima  5028  mptpreima  5032  dfco2  5038  coundi  5040  coundir  5041  resco  5043  imaco  5044  rnco  5045  coiun  5048  coi1  5054  coass  5057  xpcom  5085  dffun2  5133  imadif  5203  imainlem  5204  funimaexglem  5206  fun11iun  5388  f11o  5400  brprcneu  5414  nfvres  5454  fndmin  5527  abrexco  5660  imaiun  5661  dfoprab2  5818  cbvoprab2  5844  rexrnmpo  5886  opabex3d  6019  opabex3  6020  abexssex  6023  abexex  6024  oprabrexex2  6028  releldm2  6083  dfopab2  6087  dfoprab3s  6088  cnvoprab  6131  brtpos2  6148  tfr1onlemaccex  6245  tfrcllembxssdm  6253  tfrcllemaccex  6258  domen  6645  mapsnen  6705  xpsnen  6715  xpcomco  6720  xpassen  6724  fimax2gtri  6795  supelti  6889  subhalfnqq  7222  ltbtwnnq  7224  prnmaxl  7296  prnminu  7297  prarloc  7311  genpdflem  7315  genpassl  7332  genpassu  7333  ltexprlemm  7408  2rexuz  9377  seq3f1olemp  10275  cbvsum  11129  cbvprod  11327  inffinp1  11942  unct  11954  isbasis2g  12212  tgval2  12220  ntreq0  12301  lmff  12418  metrest  12675  bj-axempty  13091  bj-axempty2  13092  bj-vprc  13094  bdinex1  13097  bj-zfpair2  13108  bj-uniex2  13114  bj-d0clsepcl  13123