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

Theorem wel 1868
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 1868 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 1867. This lets us avoid overloading the  e. connective, thus preventing ambiguity that would complicate certain Metamath parsers. However, logically wel 1868 is considered to be a primitive syntax, even though here it is artificially "derived" from wcel 1867. 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 1867 1  wff  x  e.  y
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1867
This theorem is referenced by:  elequ1  1870  elequ2  1872  ax12wdemo  1880  cleljust  2160  cleljustALT  2161  dveel1  2162  dveel2  2163  axc14  2164  elsb3  2227  elsb4  2228  axext2  2399  axext3  2400  axext3OLD  2401  axext4  2402  bm1.1  2403  bm1.1OLD  2404  sbabel  2614  ru  3295  nfuni  4219  nfunid  4220  unieq  4221  csbuni  4241  inteq  4252  nfint  4259  uniiun  4346  intiin  4347  trint  4526  trintss  4527  axrep1  4530  axrep2  4531  axrep3  4532  axrep4  4533  axrep5  4534  zfrepclf  4535  axsep  4538  axsep2  4540  bm1.3ii  4542  zfnuleu  4544  0ex  4548  nalset  4553  axpweq  4593  zfpow  4595  axpow2  4596  axpow3  4597  el  4598  dtru  4607  nfnid  4642  dvdemo1  4648  dvdemo2  4649  dfepfr  4830  wetrep  4838  wefrc  4839  rele  4974  ordelord  5455  funimaexg  5669  zfun  6589  axun2  6590  uniuni  6605  onint  6627  ordom  6706  wfrlem12  7046  dfsmo2  7065  smores2  7072  smo11  7082  smogt  7085  dfrecs3  7090  tz7.48lem  7157  tz7.48-2  7158  omeulem1  7282  pw2eng  7675  infensuc  7747  1sdom  7772  unxpdomlem1  7773  unxpdomlem2  7774  unxpdomlem3  7775  pssnn  7787  findcard2  7808  findcard2d  7810  ac6sfi  7812  frfi  7813  fissuni  7876  axreg2  8099  zfregcl  8100  dford2  8116  inf0  8117  inf1  8118  inf2  8119  zfinf  8135  axinf2  8136  zfinf2  8138  dfom4  8145  dfom5  8146  unbnn3  8154  noinfep  8155  cantnf  8188  epfrs  8205  r111  8236  dif1card  8431  alephle  8508  aceq1  8537  aceq0  8538  aceq2  8539  dfac3  8541  dfac5lem2  8544  dfac5lem4  8546  dfac5  8548  dfac2a  8549  dfac2  8550  dfac7  8551  dfac0  8552  dfac1  8553  kmlem3  8571  kmlem4  8572  kmlem5  8573  kmlem8  8576  kmlem14  8582  kmlem15  8583  dfackm  8585  ackbij1lem10  8648  coflim  8680  cflim2  8682  cfsmolem  8689  fin23lem26  8744  ituniiun  8841  domtriomlem  8861  axdc3lem2  8870  zfac  8879  ac2  8880  ac3  8881  axac3  8883  axac2  8885  axac  8886  nd1  9001  nd2  9002  nd3  9003  nd4  9004  axextnd  9005  axrepndlem1  9006  axrepndlem2  9007  axrepnd  9008  axunndlem1  9009  axunnd  9010  axpowndlem1  9011  axpowndlem2  9012  axpowndlem3  9013  axpowndlem4  9014  axpownd  9015  axregndlem1  9016  axregndlem2  9017  axregnd  9018  axinfndlem1  9019  axinfnd  9020  axacndlem1  9021  axacndlem2  9022  axacndlem3  9023  axacndlem4  9024  axacndlem5  9025  axacnd  9026  fpwwe2lem12  9055  axgroth5  9238  axgroth2  9239  grothpw  9240  axgroth6  9242  grothomex  9243  axgroth3  9245  axgroth4  9246  grothprimlem  9247  grothprim  9248  nqereu  9343  npex  9400  elnpi  9402  hashbclem  12599  brfi1uzind  12630  fsum2dlem  13798  fprod2dlem  14001  fprod2d  14002  rpnnen  14246  lcmfunsnlem2lem2  14572  ismre  15440  fnmre  15441  mremre  15454  isacs  15501  isacs1i  15507  mreacs  15508  acsfn1  15511  acsfn2  15513  isacs3lem  16356  pmtrprfval  17072  pmtrsn  17104  gsum2dlem2  17531  lbsextlem4  18312  drngnidl  18381  mplcoe1  18617  mplcoe5  18620  zringlpir  18983  mdetunilem9  19569  mdetuni0  19570  maducoeval2  19589  madugsum  19592  isbasis3g  19888  tgcl  19909  tgss2  19927  toponmre  20033  neiptopnei  20072  ist0  20260  ishaus  20262  t0top  20269  haustop  20271  isreg  20272  ist0-2  20284  ist0-3  20285  t1t0  20288  ist1-3  20289  ishaus2  20291  haust1  20292  cmpsublem  20338  cmpsub  20339  tgcmp  20340  hauscmp  20346  bwth  20349  is1stc2  20381  2ndcctbss  20394  2ndcdisj  20395  2ndcdisj2  20396  2ndcomap  20397  2ndcsep  20398  dis2ndc  20399  restnlly  20421  restlly  20422  llyidm  20427  nllyidm  20428  lly1stc  20435  finptfin  20457  locfincmp  20465  ptpjopn  20551  tx1stc  20589  txkgen  20591  xkohaus  20592  xkococnlem  20598  xkoinjcn  20626  ist0-4  20668  kqt0lem  20675  regr1lem2  20679  kqt0  20685  r0sep  20687  nrmr0reg  20688  regr1  20689  kqreg  20690  kqnrm  20691  kqhmph  20758  filuni  20824  uffinfix  20866  fmfnfmlem4  20896  hauspwpwf1  20926  alexsublem  20983  alexsubALTlem3  20988  alexsubALTlem4  20989  alexsubALT  20990  blbas  21369  met1stc  21460  metrest  21463  xrsmopn  21734  cnheibor  21872  jensen  23776  sqff1o  23969  usgrafis  24985  cusgrasize  25048  dfconngra1  25241  0egra0rgra  25506  isplig  25751  tncp  25752  spanuni  27029  sumdmdii  27900  gsumvsca2  28382  indf1o  28681  gsumesum  28716  dya2iocuni  28941  bnj219  29326  bnj1098  29380  bnj594  29508  bnj580  29509  bnj601  29516  bnj849  29521  bnj996  29551  bnj1006  29555  bnj1029  29562  bnj1033  29563  bnj1090  29573  bnj1110  29576  bnj1124  29582  bnj1128  29584  erdsze  29710  conpcon  29743  rellyscon  29759  cvmsss2  29782  cvmlift2lem12  29822  axextprim  30113  axrepprim  30114  axunprim  30115  axpowprim  30116  axregprim  30117  axinfprim  30118  axacprim  30119  untelirr  30120  untuni  30121  untsucf  30122  unt0  30123  untint  30124  untangtr  30126  dftr6  30174  dffr5  30177  elpotr  30211  dfon2lem3  30215  dfon2lem4  30216  dfon2lem5  30217  dfon2lem6  30218  dfon2lem7  30219  dfon2lem8  30220  dfon2lem9  30221  dfon2  30222  domep  30223  axextdfeq  30228  ax8dfeq  30229  axextdist  30230  axext4dist  30231  exnel  30233  distel  30234  axextndbi  30235  poseq  30275  frrlem11  30310  nobndlem6  30368  nofulllem5  30377  dfiota3  30472  brcup  30488  brcap  30489  dfint3  30501  imagesset  30502  hftr  30731  fness  30787  fneref  30788  neibastop2lem  30798  onsuct0  30883  bj-elequ2g  31014  bj-ax89  31015  bj-elequ12  31016  bj-cleljust  31121  bj-axext3  31131  bj-axext4  31132  bj-clabel  31146  bj-axrep1  31151  bj-axrep2  31152  bj-axrep3  31153  bj-axrep4  31154  bj-axrep5  31155  bj-axsep  31156  bj-nalset  31157  bj-zfpow  31158  bj-el  31159  bj-dtru  31160  bj-dvdemo1  31165  bj-dvdemo2  31166  bj-ax8  31242  bj-ax9  31245  bj-cleqhyp  31246  bj-axsep2  31275  bj-ru0  31283  bj-ru1  31284  bj-ru  31285  bj-nul  31367  bj-nuliota  31368  bj-nuliotaALT  31369  finixpnum  31634  fin2solem  31635  fin2so  31636  poimirlem30  31674  poimirlem32  31676  poimir  31677  heicant  31679  mblfinlem1  31681  mbfresfi  31691  cnambfre  31693  ftc1anc  31729  ftc2nc  31730  cover2g  31745  sstotbnd2  31810  unichnidl  31968  prtlem5  32136  prtlem12  32147  prtlem13  32148  prtlem15  32155  prtlem17  32156  prtlem18  32157  prter1  32159  prter3  32162  ax5el  32217  dveel2ALT  32219  ax12el  32222  pclfinclN  33224  dvh1dim  34719  ismrcd1  35249  dford3lem2  35592  dford4  35594  pw2f1ocnv  35602  pw2f1o2  35603  wepwsolem  35610  fnwe2lem2  35619  aomclem8  35629  kelac1  35631  pwslnm  35662  idomsubgmo  35775  elintima  35888  dffrege76  36176  frege77  36177  frege89  36189  frege90  36190  frege91  36191  frege93  36193  frege94  36194  frege95  36195  sbcoreleleq  36537  tratrb  36538  ordelordALT  36539  trsbc  36542  truniALT  36543  onfrALTlem5  36549  onfrALTlem4  36550  onfrALTlem3  36551  onfrALTlem2  36553  onfrALTlem1  36555  onfrALT  36556  sspwtrALT  36854  suctrALT2  36877  tratrbVD  36902  truniALTVD  36919  trintALT  36922  onfrALTlem4VD  36927  usgfis  38529  dflinc2  38976  lcosslsp  39004
  Copyright terms: Public domain W3C validator