ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  exbii GIF version

Theorem exbii 1496
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
StepHypRef Expression
1 exbi 1495 . 2 (∀𝑥(𝜑𝜓) → (∃𝑥𝜑 ↔ ∃𝑥𝜓))
2 exbii.1 . 2 (𝜑𝜓)
31, 2mpg 1340 1 (∃𝑥𝜑 ↔ ∃𝑥𝜓)
Colors of variables: wff set class
Syntax hints:  wb 98  wex 1381
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1336  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-4 1400  ax-ial 1427
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  2exbii  1497  3exbii  1498  exancom  1499  excom13  1579  exrot4  1581  eeor  1585  sbcof2  1691  sbequ8  1727  sbidm  1731  sborv  1770  19.41vv  1783  19.41vvv  1784  19.41vvvv  1785  exdistr  1787  19.42vvv  1789  exdistr2  1791  3exdistr  1792  4exdistr  1793  eean  1806  eeeanv  1808  ee4anv  1809  2sb5  1859  2sb5rf  1865  sbel2x  1874  sbexyz  1879  sbex  1880  exsb  1884  2exsb  1885  sb8eu  1913  sb8euh  1923  eu1  1925  eu2  1944  2moswapdc  1990  2exeu  1992  exists1  1996  clelab  2162  clabel  2163  sbabel  2203  rexbii2  2335  r2exf  2342  nfrexdya  2359  r19.41  2465  r19.43  2468  isset  2561  rexv  2572  ceqsex2  2594  ceqsex3v  2596  gencbvex  2600  ceqsrexv  2674  rexab  2703  rexrab2  2708  euxfrdc  2727  euind  2728  reu6  2730  reu3  2731  2reuswapdc  2743  reuind  2744  sbccomlem  2832  rmo2ilem  2847  rexun  3123  reupick3  3222  abn0r  3243  rabn0m  3245  rexsns  3409  rexsnsOLD  3410  exsnrex  3413  snprc  3435  euabsn2  3439  reusn  3441  eusn  3444  elunirab  3593  unipr  3594  uniun  3599  uniin  3600  iuncom4  3664  dfiun2g  3689  iunn0m  3717  iunxiun  3736  cbvopab2  3831  cbvopab2v  3834  unopab  3836  zfnuleu  3881  0ex  3884  vprc  3888  inex1  3891  intexabim  3906  iinexgm  3908  inuni  3909  unidif0  3920  axpweq  3924  zfpow  3928  axpow2  3929  axpow3  3930  pwex  3932  zfpair2  3945  mss  3962  exss  3963  opm  3971  eqvinop  3980  copsexg  3981  opabm  4017  iunopab  4018  zfun  4171  uniex2  4173  uniuni  4183  rexxfrd  4195  dtruex  4283  zfinf2  4312  elxp2  4363  opeliunxp  4395  xpiundi  4398  xpiundir  4399  elvvv  4403  eliunxp  4475  rexiunxp  4478  relop  4486  opelco2g  4503  cnvco  4520  cnvuni  4521  dfdm3  4522  dfrn2  4523  dfrn3  4524  elrng  4526  dfdm4  4527  eldm2g  4531  dmun  4542  dmin  4543  dmiun  4544  dmuni  4545  dmopab  4546  dmi  4550  dmmrnm  4554  elrn  4577  rnopab  4581  dmcosseq  4603  dmres  4632  elres  4646  elsnres  4647  dfima2  4670  elima3  4675  imadmrn  4678  imai  4681  args  4694  rniun  4734  ssrnres  4763  dmsnm  4786  dmsnopg  4792  elxp4  4808  elxp5  4809  cnvresima  4810  mptpreima  4814  dfco2  4820  coundi  4822  coundir  4823  resco  4825  imaco  4826  rnco  4827  coiun  4830  coi1  4836  coass  4839  xpcom  4864  dffun2  4912  imadif  4979  imainlem  4980  funimaexglem  4982  fun11iun  5147  f11o  5159  brprcneu  5171  nfvres  5206  fndmin  5274  abrexco  5398  imaiun  5399  dfoprab2  5552  cbvoprab2  5577  rexrnmpt2  5616  opabex3d  5748  opabex3  5749  abexssex  5752  abexex  5753  oprabrexex2  5757  releldm2  5811  dfopab2  5815  dfoprab3s  5816  brtpos2  5866  domen  6232  xpsnen  6295  xpcomco  6300  xpassen  6304  subhalfnqq  6510  ltbtwnnq  6512  prnmaxl  6584  prnminu  6585  prarloc  6599  genpdflem  6603  genpassl  6620  genpassu  6621  ltexprlemm  6696  2rexuz  8523  bj-axempty  9987  bj-axempty2  9988  bj-vprc  9990  bdinex1  9993  bj-zfpair2  10004  bj-uniex2  10010  bj-d0clsepcl  10023
  Copyright terms: Public domain W3C validator