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

Theorem exbii 1605
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 1604 . 2 (∀𝑥(𝜑𝜓) → (∃𝑥𝜑 ↔ ∃𝑥𝜓))
2 exbii.1 . 2 (𝜑𝜓)
31, 2mpg 1451 1 (∃𝑥𝜑 ↔ ∃𝑥𝜓)
Colors of variables: wff set class
Syntax hints:  wb 105  wex 1492
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 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510  ax-ial 1534
This theorem depends on definitions:  df-bi 117
This theorem is referenced by:  2exbii  1606  3exbii  1607  exancom  1608  excom13  1689  exrot4  1691  eeor  1695  sbcof2  1810  sbequ8  1847  sbidm  1851  sborv  1890  19.41vv  1903  19.41vvv  1904  19.41vvvv  1905  exdistr  1909  19.42vvv  1912  exdistr2  1914  3exdistr  1915  4exdistr  1916  eean  1931  eeeanv  1933  ee4anv  1934  2sb5  1983  2sb5rf  1989  sbel2x  1998  sbexyz  2003  sbex  2004  exsb  2008  2exsb  2009  sb8eu  2039  sb8euh  2049  eu1  2051  eu2  2070  2moswapdc  2116  2exeu  2118  exists1  2122  clelab  2303  clabel  2304  sbabel  2346  rexbii2  2488  r2exf  2495  nfrexdya  2513  r19.41  2632  r19.43  2635  cbvreuvw  2709  isset  2743  rexv  2755  ceqsex2  2777  ceqsex3v  2779  gencbvex  2783  ceqsrexv  2867  rexab  2899  rexrab2  2904  euxfrdc  2923  euind  2924  reu6  2926  reu3  2927  2reuswapdc  2941  reuind  2942  sbccomlem  3037  rmo2ilem  3052  rexun  3315  reupick3  3420  abn0r  3447  abn0m  3448  rabn0m  3450  rexsns  3630  exsnrex  3633  snprc  3656  euabsn2  3660  reusn  3662  eusn  3665  elunirab  3820  unipr  3821  uniun  3826  uniin  3827  iuncom4  3891  dfiun2g  3916  iunn0m  3944  iunxiun  3965  disjnim  3991  cbvopab2  4074  cbvopab2v  4077  unopab  4079  zfnuleu  4124  0ex  4127  vnex  4131  inex1  4134  intexabim  4149  iinexgm  4151  inuni  4152  unidif0  4164  axpweq  4168  zfpow  4172  axpow2  4173  axpow3  4174  vpwex  4176  zfpair2  4207  mss  4223  exss  4224  opm  4231  eqvinop  4240  copsexg  4241  opabm  4277  iunopab  4278  zfun  4431  uniex2  4433  uniuni  4448  rexxfrd  4460  dtruex  4555  zfinf2  4585  elxp2  4641  opeliunxp  4678  xpiundi  4681  xpiundir  4682  elvvv  4686  eliunxp  4762  rexiunxp  4765  relop  4773  elco  4789  opelco2g  4791  cnvco  4808  cnvuni  4809  dfdm3  4810  dfrn2  4811  dfrn3  4812  elrng  4814  dfdm4  4815  eldm2g  4819  dmun  4830  dmin  4831  dmiun  4832  dmuni  4833  dmopab  4834  dmi  4838  dmmrnm  4842  elrn  4866  rnopab  4870  dmcosseq  4894  dmres  4924  elres  4939  elsnres  4940  dfima2  4968  elima3  4973  imadmrn  4976  imai  4980  args  4993  rniun  5035  ssrnres  5067  dmsnm  5090  dmsnopg  5096  elxp4  5112  elxp5  5113  cnvresima  5114  mptpreima  5118  dfco2  5124  coundi  5126  coundir  5127  resco  5129  imaco  5130  rnco  5131  coiun  5134  coi1  5140  coass  5143  xpcom  5171  dffun2  5222  imadif  5292  imainlem  5293  funimaexglem  5295  fun11iun  5478  f11o  5490  brprcneu  5504  nfvres  5544  fndmin  5619  abrexco  5754  imaiun  5755  dfoprab2  5916  cbvoprab2  5942  rexrnmpo  5984  opabex3d  6116  opabex3  6117  abexssex  6120  abexex  6121  oprabrexex2  6125  releldm2  6180  dfopab2  6184  dfoprab3s  6185  cnvoprab  6229  brtpos2  6246  tfr1onlemaccex  6343  tfrcllembxssdm  6351  tfrcllemaccex  6356  domen  6745  mapsnen  6805  xpsnen  6815  xpcomco  6820  xpassen  6824  fimax2gtri  6895  supelti  6995  cc1  7252  subhalfnqq  7401  ltbtwnnq  7403  prnmaxl  7475  prnminu  7476  prarloc  7490  genpdflem  7494  genpassl  7511  genpassu  7512  ltexprlemm  7587  2rexuz  9568  seq3f1olemp  10485  cbvsum  11349  cbvprod  11547  nnwosdc  12020  inffinp1  12410  ctiunctal  12422  unct  12423  isbasis2g  13203  tgval2  13211  ntreq0  13292  lmff  13409  metrest  13666  bj-axempty  14294  bj-axempty2  14295  bj-vprc  14297  bdinex1  14300  bj-zfpair2  14311  bj-uniex2  14317  bj-d0clsepcl  14326
  Copyright terms: Public domain W3C validator