Theorem exbii 1619

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

Syntax hints:   ↔ wb 105  ∃wex 1506

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 1461  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-4 1524  ax-ial 1548

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  2exbii  1620  3exbii  1621  exancom  1622  excom13  1703  exrot4  1705  eeor  1709  sbcof2  1824  sbequ8  1861  sbidm  1865  sborv  1905  19.41vv  1918  19.41vvv  1919  19.41vvvv  1920  exdistr  1924  19.42vvv  1927  exdistr2  1929  3exdistr  1930  4exdistr  1931  eean  1950  eeeanv  1952  ee4anv  1953  2sb5  2002  2sb5rf  2008  sbel2x  2017  sbexyz  2022  sbex  2023  exsb  2027  2exsb  2028  sb8eu  2058  sb8euh  2068  eu1  2070  eu2  2089  2moswapdc  2135  2exeu  2137  exists1  2141  clelab  2322  clabel  2323  sbabel  2366  rexbii2  2508  r2exf  2515  nfrexdya  2533  r19.41  2652  r19.43  2655  cbvreuvw  2735  isset  2769  rexv  2781  ceqsex2  2804  ceqsex3v  2806  gencbvex  2810  ceqsrexv  2894  rexab  2926  rexrab2  2931  euxfrdc  2950  euind  2951  reu6  2953  reu3  2954  2reuswapdc  2968  reuind  2969  sbccomlem  3064  rmo2ilem  3079  rexun  3343  reupick3  3448  abn0r  3475  abn0m  3476  rabn0m  3478  rexsns  3661  exsnrex  3664  snprc  3687  euabsn2  3691  reusn  3693  eusn  3696  elunirab  3852  unipr  3853  uniun  3858  uniin  3859  iuncom4  3923  dfiun2g  3948  iunn0m  3977  iunxiun  3998  disjnim  4024  cbvopab2  4107  cbvopab2v  4110  unopab  4112  zfnuleu  4157  0ex  4160  vnex  4164  inex1  4167  intexabim  4185  iinexgm  4187  inuni  4188  unidif0  4200  axpweq  4204  zfpow  4208  axpow2  4209  axpow3  4210  vpwex  4212  zfpair2  4243  mss  4259  exss  4260  opm  4267  eqvinop  4276  copsexg  4277  opabm  4315  iunopab  4316  zfun  4469  uniex2  4471  uniuni  4486  rexxfrd  4498  dtruex  4595  zfinf2  4625  elxp2  4681  opeliunxp  4718  xpiundi  4721  xpiundir  4722  elvvv  4726  eliunxp  4805  rexiunxp  4808  relop  4816  elco  4832  opelco2g  4834  cnvco  4851  cnvuni  4852  dfdm3  4853  dfrn2  4854  dfrn3  4855  elrng  4857  dfdm4  4858  eldm2g  4862  dmun  4873  dmin  4874  dmiun  4875  dmuni  4876  dmopab  4877  dmi  4881  dmmrnm  4885  elrn  4909  rnopab  4913  dmcosseq  4937  dmres  4967  elres  4982  elsnres  4983  dfima2  5011  elima3  5016  imadmrn  5019  imai  5025  args  5038  rniun  5080  ssrnres  5112  dmsnm  5135  dmsnopg  5141  elxp4  5157  elxp5  5158  cnvresima  5159  mptpreima  5163  dfco2  5169  coundi  5171  coundir  5172  resco  5174  imaco  5175  rnco  5176  coiun  5179  coi1  5185  coass  5188  xpcom  5216  dffun2  5268  imadif  5338  imainlem  5339  funimaexglem  5341  fun11iun  5525  f11o  5537  brprcneu  5551  nfvres  5592  fndmin  5669  abrexco  5806  imaiun  5807  dfoprab2  5969  cbvoprab2  5995  rexrnmpo  6038  opabex3d  6178  opabex3  6179  abexssex  6182  abexex  6183  oprabrexex2  6187  uchoice  6195  releldm2  6243  dfopab2  6247  dfoprab3s  6248  cnvoprab  6292  brtpos2  6309  tfr1onlemaccex  6406  tfrcllembxssdm  6414  tfrcllemaccex  6419  domen  6810  mapsnen  6870  xpsnen  6880  xpcomco  6885  xpassen  6889  fimax2gtri  6962  supelti  7068  cc1  7332  subhalfnqq  7481  ltbtwnnq  7483  prnmaxl  7555  prnminu  7556  prarloc  7570  genpdflem  7574  genpassl  7591  genpassu  7592  ltexprlemm  7667  2rexuz  9656  seq3f1olemp  10607  cbvsum  11525  cbvprod  11723  nnwosdc  12206  4sqlem12  12571  inffinp1  12646  ctiunctal  12658  unct  12659  isbasis2g  14281  tgval2  14287  ntreq0  14368  lmff  14485  metrest  14742  bj-axempty  15539  bj-axempty2  15540  bj-vprc  15542  bdinex1  15545  bj-zfpair2  15556  bj-uniex2  15562  bj-d0clsepcl  15571