Theorem exbii 1654

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

Syntax hints:   ↔ wb 105  ∃wex 1541

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 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-ial 1583

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  2exbii  1655  3exbii  1656  exancom  1657  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  2358  clabel  2359  sbabel  2402  rexbii2  2544  r2exf  2551  nfrexdya  2569  r19.41  2689  r19.43  2692  cbvreuvw  2774  isset  2810  rexv  2822  ceqsex2  2845  ceqsex3v  2847  gencbvex  2851  ceqsrexv  2937  rexab  2969  rexrab2  2974  euxfrdc  2993  euind  2994  reu6  2996  reu3  2997  2reuswapdc  3011  reuind  3012  sbccomlem  3107  rmo2ilem  3123  rexun  3389  reupick3  3494  abn0r  3521  abn0m  3522  rabn0m  3524  rexsns  3712  exsnrex  3715  snprc  3738  euabsn2  3744  reusn  3746  eusn  3749  snmb  3797  elunirab  3911  unipr  3912  uniun  3917  uniin  3918  iuncom4  3982  dfiun2g  4007  iunn0m  4036  iunxiun  4057  disjnim  4083  cbvopab2  4168  cbvopab2v  4171  unopab  4173  zfnuleu  4218  0ex  4221  vnex  4225  inex1  4228  intexabim  4247  iinexgm  4249  inuni  4250  unidif0  4263  axpweq  4267  zfpow  4271  axpow2  4272  axpow3  4273  vpwex  4275  zfpair2  4306  mss  4324  exss  4325  opm  4332  eqvinop  4341  copsexg  4342  opabm  4381  iunopab  4382  zfun  4537  uniex2  4539  uniuni  4554  rexxfrd  4566  dtruex  4663  zfinf2  4693  elxp2  4749  opeliunxp  4787  xpiundi  4790  xpiundir  4791  elvvv  4795  eliunxp  4875  rexiunxp  4878  relop  4886  elco  4902  opelco2g  4904  cnvco  4921  cnvuni  4922  dfdm3  4923  dfrn2  4924  dfrn3  4925  elrng  4927  dfdm4  4929  eldm2g  4933  dmun  4944  dmin  4945  dmiun  4946  dmuni  4947  dmopab  4948  dmi  4952  reldmm  4956  dmmrnm  4957  elrn  4981  rnopab  4985  dmcosseq  5010  dmres  5040  elres  5055  elsnres  5056  dfima2  5084  elima3  5089  imadmrn  5092  imai  5099  args  5112  rniun  5154  ssrnres  5186  dmsnm  5209  dmsnopg  5215  elxp4  5231  elxp5  5232  cnvresima  5233  mptpreima  5237  dfco2  5243  coundi  5245  coundir  5246  resco  5248  imaco  5249  rnco  5250  coiun  5253  coi1  5259  coass  5262  xpcom  5290  dffun2  5343  imadif  5417  imainlem  5418  funimaexglem  5420  fun11iun  5613  f11o  5626  brprcneu  5641  nfvres  5684  fndmin  5763  abrexco  5910  imaiun  5911  dfoprab2  6078  cbvoprab2  6104  rexrnmpo  6147  opabex3d  6292  opabex3  6293  abexssex  6296  abexex  6297  oprabrexex2  6301  uchoice  6309  releldm2  6357  dfopab2  6361  dfoprab3s  6362  cnvoprab  6408  cnvimadfsn  6423  brtpos2  6460  tfr1onlemaccex  6557  tfrcllembxssdm  6565  tfrcllemaccex  6570  domen  6965  mapsnen  7029  xpsnen  7048  xpcomco  7053  xpassen  7057  fimax2gtri  7134  supelti  7244  cc1  7527  subhalfnqq  7677  ltbtwnnq  7679  prnmaxl  7751  prnminu  7752  prarloc  7766  genpdflem  7770  genpassl  7787  genpassu  7788  ltexprlemm  7863  2rexuz  9860  seq3f1olemp  10823  cbvsum  11983  cbvprod  12182  nnwosdc  12673  4sqlem12  13038  inffinp1  13113  ctiunctal  13125  unct  13126  isbasis2g  14839  tgval2  14845  ntreq0  14926  lmff  15043  metrest  15300  upgrex  16027  1loopgrvd2fi  16229  bj-axempty  16592  bj-axempty2  16593  bj-vprc  16595  bdinex1  16598  bj-zfpair2  16609  bj-uniex2  16615  bj-d0clsepcl  16624