Theorem exbii 1653

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

Syntax hints:   ↔ wb 105  ∃wex 1540

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 1495  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-4 1558  ax-ial 1582

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  2exbii  1654  3exbii  1655  exancom  1656  excom13  1737  exrot4  1739  eeor  1743  sbcof2  1858  sbequ8  1895  sbidm  1899  sborv  1939  19.41vv  1952  19.41vvv  1953  19.41vvvv  1954  exdistr  1958  19.42vvv  1961  exdistr2  1963  3exdistr  1964  4exdistr  1965  eean  1984  eeeanv  1986  ee4anv  1987  2sb5  2036  2sb5rf  2042  sbel2x  2051  sbexyz  2056  sbex  2057  exsb  2061  2exsb  2062  sb8eu  2092  sb8euh  2102  eu1  2104  eu2  2124  2moswapdc  2170  2exeu  2172  exists1  2176  clelab  2357  clabel  2358  sbabel  2401  rexbii2  2543  r2exf  2550  nfrexdya  2568  r19.41  2688  r19.43  2691  cbvreuvw  2773  isset  2809  rexv  2821  ceqsex2  2844  ceqsex3v  2846  gencbvex  2850  ceqsrexv  2936  rexab  2968  rexrab2  2973  euxfrdc  2992  euind  2993  reu6  2995  reu3  2996  2reuswapdc  3010  reuind  3011  sbccomlem  3106  rmo2ilem  3122  rexun  3387  reupick3  3492  abn0r  3519  abn0m  3520  rabn0m  3522  rexsns  3708  exsnrex  3711  snprc  3734  euabsn2  3740  reusn  3742  eusn  3745  snmb  3793  elunirab  3906  unipr  3907  uniun  3912  uniin  3913  iuncom4  3977  dfiun2g  4002  iunn0m  4031  iunxiun  4052  disjnim  4078  cbvopab2  4163  cbvopab2v  4166  unopab  4168  zfnuleu  4213  0ex  4216  vnex  4220  inex1  4223  intexabim  4242  iinexgm  4244  inuni  4245  unidif0  4257  axpweq  4261  zfpow  4265  axpow2  4266  axpow3  4267  vpwex  4269  zfpair2  4300  mss  4318  exss  4319  opm  4326  eqvinop  4335  copsexg  4336  opabm  4375  iunopab  4376  zfun  4531  uniex2  4533  uniuni  4548  rexxfrd  4560  dtruex  4657  zfinf2  4687  elxp2  4743  opeliunxp  4781  xpiundi  4784  xpiundir  4785  elvvv  4789  eliunxp  4869  rexiunxp  4872  relop  4880  elco  4896  opelco2g  4898  cnvco  4915  cnvuni  4916  dfdm3  4917  dfrn2  4918  dfrn3  4919  elrng  4921  dfdm4  4923  eldm2g  4927  dmun  4938  dmin  4939  dmiun  4940  dmuni  4941  dmopab  4942  dmi  4946  reldmm  4950  dmmrnm  4951  elrn  4975  rnopab  4979  dmcosseq  5004  dmres  5034  elres  5049  elsnres  5050  dfima2  5078  elima3  5083  imadmrn  5086  imai  5092  args  5105  rniun  5147  ssrnres  5179  dmsnm  5202  dmsnopg  5208  elxp4  5224  elxp5  5225  cnvresima  5226  mptpreima  5230  dfco2  5236  coundi  5238  coundir  5239  resco  5241  imaco  5242  rnco  5243  coiun  5246  coi1  5252  coass  5255  xpcom  5283  dffun2  5336  imadif  5410  imainlem  5411  funimaexglem  5413  fun11iun  5604  f11o  5617  brprcneu  5632  nfvres  5675  fndmin  5754  abrexco  5899  imaiun  5900  dfoprab2  6067  cbvoprab2  6093  rexrnmpo  6136  opabex3d  6282  opabex3  6283  abexssex  6286  abexex  6287  oprabrexex2  6291  uchoice  6299  releldm2  6347  dfopab2  6351  dfoprab3s  6352  cnvoprab  6398  brtpos2  6416  tfr1onlemaccex  6513  tfrcllembxssdm  6521  tfrcllemaccex  6526  domen  6921  mapsnen  6985  xpsnen  7004  xpcomco  7009  xpassen  7013  fimax2gtri  7090  supelti  7200  cc1  7483  subhalfnqq  7633  ltbtwnnq  7635  prnmaxl  7707  prnminu  7708  prarloc  7722  genpdflem  7726  genpassl  7743  genpassu  7744  ltexprlemm  7819  2rexuz  9815  seq3f1olemp  10776  cbvsum  11920  cbvprod  12118  nnwosdc  12609  4sqlem12  12974  inffinp1  13049  ctiunctal  13061  unct  13062  isbasis2g  14768  tgval2  14774  ntreq0  14855  lmff  14972  metrest  15229  upgrex  15953  1loopgrvd2fi  16155  bj-axempty  16488  bj-axempty2  16489  bj-vprc  16491  bdinex1  16494  bj-zfpair2  16505  bj-uniex2  16511  bj-d0clsepcl  16520