MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  wel Structured version   Unicode version

Theorem wel 1803
Description: Extend wff definition to include atomic formulas with the epsilon (membership) predicate. This is read " x is an element of  y," " x is a member of  y," " x belongs to  y," or " y contains  x." Note: The phrase " y includes  x " means " x is a subset of  y;" to use it also for  x  e.  y, as some authors occasionally do, is poor form and causes confusion, according to George Boolos (1992 lecture at MIT).

This syntactical construction introduces a binary non-logical predicate symbol  e. (epsilon) into our predicate calculus. We will eventually use it for the membership predicate of set theory, but that is irrelevant at this point: the predicate calculus axioms for  e. apply to any arbitrary binary predicate symbol. "Non-logical" means that the predicate is presumed to have additional properties beyond the realm of predicate calculus, although these additional properties are not specified by predicate calculus itself but rather by the axioms of a theory (in our case set theory) added to predicate calculus. "Binary" means that the predicate has two arguments.

(Instead of introducing wel 1803 as an axiomatic statement, as was done in an older version of this database, we introduce it by "proving" a special case of set theory's more general wcel 1802. This lets us avoid overloading the  e. connective, thus preventing ambiguity that would complicate certain Metamath parsers. However, logically wel 1803 is considered to be a primitive syntax, even though here it is artificially "derived" from wcel 1802. Note: To see the proof steps of this syntax proof, type "show proof wel /all" in the Metamath program.) (Contributed by NM, 24-Jan-2006.)

Assertion
Ref Expression
wel  wff  x  e.  y

Proof of Theorem wel
StepHypRef Expression
1 wcel 1802 1  wff  x  e.  y
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1802
This theorem is referenced by:  elequ1  1805  elequ2  1807  ax12wdemo  1815  cleljust  2093  cleljustALT  2094  dveel1  2095  dveel2  2096  axc14  2097  elsb3  2162  elsb4  2163  ax5el  2251  dveel2ALT  2253  ax12el  2256  axext2  2420  axext3  2421  axext3OLD  2422  axext4  2423  bm1.1  2424  bm1.1OLD  2425  sbabel  2634  ru  3310  nfuni  4237  nfunid  4238  unieq  4239  csbuni  4259  inteq  4271  nfint  4278  uniiun  4365  intiin  4366  trint  4542  trintss  4543  axrep1  4546  axrep2  4547  axrep3  4548  axrep4  4549  axrep5  4550  zfrepclf  4551  axsep  4554  axsep2  4556  bm1.3ii  4558  zfnuleu  4560  0ex  4564  nalset  4571  axpweq  4611  zfpow  4613  axpow2  4614  axpow3  4615  el  4616  dtru  4625  nfnid  4663  dvdemo1  4669  dvdemo2  4670  dfepfr  4851  wetrep  4859  wefrc  4860  ordelord  4887  rele  5118  funimaexg  5652  zfun  6575  axun2  6576  uniuni  6591  onint  6612  ordom  6691  dfsmo2  7017  smores2  7024  smo11  7034  smogt  7037  tz7.48lem  7105  tz7.48-2  7106  omeulem1  7230  pw2eng  7622  infensuc  7694  1sdom  7721  unxpdomlem1  7723  unxpdomlem2  7724  unxpdomlem3  7725  pssnn  7737  findcard2  7759  findcard2d  7761  ac6sfi  7763  frfi  7764  fissuni  7824  axreg2  8019  zfregcl  8020  dford2  8037  inf0  8038  inf1  8039  inf2  8040  zfinf  8056  axinf2  8057  zfinf2  8059  dfom4  8066  dfom5  8067  unbnn3  8075  noinfep  8076  cantnf  8112  cantnfOLD  8134  epfrs  8162  r111  8193  dif1card  8388  alephle  8469  aceq1  8498  aceq0  8499  aceq2  8500  dfac3  8502  dfac5lem2  8505  dfac5lem4  8507  dfac5  8509  dfac2a  8510  dfac2  8511  dfac7  8512  dfac0  8513  dfac1  8514  kmlem3  8532  kmlem4  8533  kmlem5  8534  kmlem8  8537  kmlem14  8543  kmlem15  8544  dfackm  8546  ackbij1lem10  8609  coflim  8641  cflim2  8643  cfsmolem  8650  fin23lem26  8705  ituniiun  8802  domtriomlem  8822  axdc3lem2  8831  zfac  8840  ac2  8841  ac3  8842  axac3  8844  axac2  8846  axac  8847  nd1  8962  nd2  8963  nd3  8964  nd4  8965  axextnd  8966  axrepndlem1  8967  axrepndlem2  8968  axrepnd  8969  axunndlem1  8970  axunnd  8971  axpowndlem1  8972  axpowndlem2  8973  axpowndlem2OLD  8974  axpowndlem3  8975  axpowndlem4  8977  axpownd  8978  axregndlem1  8979  axregndlem2  8980  axregnd  8981  axregndOLD  8982  axinfndlem1  8983  axinfnd  8984  axacndlem1  8985  axacndlem2  8986  axacndlem3  8987  axacndlem4  8988  axacndlem5  8989  axacnd  8990  fpwwe2lem12  9019  axgroth5  9202  axgroth2  9203  grothpw  9204  axgroth6  9206  grothomex  9207  axgroth3  9209  axgroth4  9210  grothprimlem  9211  grothprim  9212  nqereu  9307  npex  9364  elnpi  9366  hashbclem  12477  brfi1uzind  12508  fsum2dlem  13561  rpnnen  13834  ismre  14861  fnmre  14862  mremre  14875  isacs  14922  isacs1i  14928  mreacs  14929  acsfn1  14932  acsfn2  14934  isacs3lem  15667  pmtrprfval  16383  pmtrsn  16415  gsum2dlem2  16869  gsum2dOLD  16871  lbsextlem4  17678  drngnidl  17748  mplcoe1  17998  mplcoe5  18002  mplcoe2OLD  18004  zringlpir  18382  zlpir  18387  mdetunilem9  18992  mdetuni0  18993  maducoeval2  19012  madugsum  19015  isbasis3g  19320  tgcl  19341  tgss2  19359  toponmre  19464  neiptopnei  19503  ist0  19691  ishaus  19693  t0top  19700  haustop  19702  isreg  19703  ist0-2  19715  ist0-3  19716  t1t0  19719  ist1-3  19720  ishaus2  19722  haust1  19723  cmpsublem  19769  cmpsub  19770  tgcmp  19771  hauscmp  19777  bwth  19780  is1stc2  19813  2ndcctbss  19826  2ndcdisj  19827  2ndcdisj2  19828  2ndcomap  19829  2ndcsep  19830  dis2ndc  19831  restnlly  19853  restlly  19854  llyidm  19859  nllyidm  19860  lly1stc  19867  finptfin  19889  locfincmp  19897  ptpjopn  19983  tx1stc  20021  txkgen  20023  xkohaus  20024  xkococnlem  20030  xkoinjcn  20058  ist0-4  20100  kqt0lem  20107  regr1lem2  20111  kqt0  20117  r0sep  20119  nrmr0reg  20120  regr1  20121  kqreg  20122  kqnrm  20123  kqhmph  20190  filuni  20256  uffinfix  20298  fmfnfmlem4  20328  hauspwpwf1  20358  alexsublem  20414  alexsubALTlem3  20419  alexsubALTlem4  20420  alexsubALT  20421  blbas  20803  met1stc  20894  metrest  20897  xrsmopn  21187  cnheibor  21325  jensen  23187  sqff1o  23325  usgrafis  24284  cusgrasize  24347  dfconngra1  24540  0egra0rgra  24805  isplig  25048  tncp  25049  spanuni  26331  sumdmdii  27203  gsumvsca2  27644  indf1o  27907  gsumesum  27937  dya2iocuni  28124  erdsze  28516  conpcon  28550  rellyscon  28566  cvmsss2  28589  cvmlift2lem12  28629  axextprim  28943  axrepprim  28944  axunprim  28945  axpowprim  28946  axregprim  28947  axinfprim  28948  axacprim  28949  untelirr  28950  untuni  28951  untsucf  28952  unt0  28953  untint  28954  untangtr  28956  fprod2dlem  29082  fprod2d  29083  dftr6  29151  dffr5  29154  elpotr  29185  dfon2lem3  29189  dfon2lem4  29190  dfon2lem5  29191  dfon2lem6  29192  dfon2lem7  29193  dfon2lem8  29194  dfon2lem9  29195  dfon2  29196  domep  29197  axextdfeq  29202  ax8dfeq  29203  axextdist  29204  axext4dist  29205  exnel  29207  distel  29208  axextndbi  29209  poseq  29305  wfrlem12  29326  frrlem11  29371  nobndlem6  29429  nofulllem5  29438  dfiota3  29545  brcup  29561  brcap  29562  tfrqfree  29573  dfint3  29574  imagesset  29575  hftr  29811  onsuct0  29878  finixpnum  30010  fin2solem  30011  fin2so  30012  heicant  30021  mblfinlem1  30023  mbfresfi  30033  cnambfre  30035  ftc1anc  30070  ftc2nc  30071  fness  30139  fneref  30140  neibastop2lem  30150  cover2g  30177  sstotbnd2  30242  unichnidl  30400  prtlem5  30569  prtlem12  30580  prtlem13  30581  prtlem15  30588  prtlem17  30589  prtlem18  30590  prter1  30592  prter3  30595  ismrcd1  30602  dford3lem2  30941  dford4  30943  pw2f1ocnv  30951  pw2f1o2  30952  wepwsolem  30959  fnwe2lem2  30969  aomclem8  30979  kelac1  30981  pwslnm  31012  idomsubgmo  31128  usgfis  32284  dflinc2  32741  lcosslsp  32769  sbcoreleleq  33034  tratrb  33035  ordelordALT  33036  trsbc  33039  truniALT  33040  onfrALTlem5  33042  onfrALTlem4  33043  onfrALTlem3  33044  onfrALTlem2  33046  onfrALTlem1  33048  onfrALT  33049  sspwtrALT  33348  suctrALT2  33365  tratrbVD  33389  truniALTVD  33406  trintALT  33409  onfrALTlem4VD  33414  bnj219  33516  bnj1098  33570  bnj594  33698  bnj580  33699  bnj601  33706  bnj849  33711  bnj996  33741  bnj1006  33745  bnj1029  33752  bnj1033  33753  bnj1090  33763  bnj1110  33766  bnj1124  33772  bnj1128  33774  bj-elequ2g  33972  bj-ax89  33973  bj-elequ12  33974  bj-cleljust  34077  bj-axext3  34087  bj-axext4  34088  bj-clabel  34102  bj-axrep1  34107  bj-axrep2  34108  bj-axrep3  34109  bj-axrep4  34110  bj-axrep5  34111  bj-axsep  34112  bj-nalset  34113  bj-zfpow  34114  bj-el  34115  bj-dtru  34116  bj-dvdemo1  34121  bj-dvdemo2  34122  bj-ax9  34197  bj-dfcleq  34199  bj-axsep2  34226  bj-ru0  34233  bj-ru1  34234  bj-ru  34235  bj-nul  34318  bj-nuliota  34319  bj-nuliotaALT  34320  pclfinclN  35397  dvh1dim  36892
  Copyright terms: Public domain W3C validator