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

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

This syntactic construction introduces a binary non-logical predicate symbol (stylized lowercase 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 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 2100 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 2099. This lets us avoid overloading the connective, thus preventing ambiguity that would complicate certain Metamath parsers. However, logically wel 2100 is considered to be a primitive syntax, even though here it is artificially "derived" from wcel 2099. Note: To see the proof steps of this syntax proof, type "MM> SHOW PROOF wel / ALL" in the Metamath program. (Contributed by NM, 24-Jan-2006.)

Assertion
Ref Expression
wel wff 𝑥𝑦

Proof of Theorem wel
StepHypRef Expression
1 wcel 2099 1 wff 𝑥𝑦
Colors of variables: wff setvar class
Syntax hints:  wcel 2099
This theorem is referenced by:  ax8  2105  elequ1  2106  elsb1  2107  cleljust  2108  ax9  2113  elequ2  2114  elequ2g  2115  elsb2  2116  ax12wdemo  2124  cleljustALT  2357  cleljustALT2  2358  dveel1  2456  dveel2  2457  axc14  2458  axexte  2700  axextg  2701  axextb  2702  axextmo  2703  nulmo  2704  cvjust  2722  ax9ALT  2723  nfcvf  2928  sbabel  2934  sbabelOLD  2935  sbralie  3350  rru  3773  ru  3774  nfunid  4910  uniprg  4920  csbuni  4935  unissb  4938  inteq  4948  elint  4951  elintg  4953  nfint  4955  int0  4961  intss  4968  intprg  4980  dfiun2g  5028  uniiun  5056  intiin  5057  dftr2c  5263  dftr5  5264  axrep1  5281  axreplem  5282  axrep2  5283  axrep3  5284  axrep4  5285  axrep5  5286  axrep6  5287  axrep6g  5288  zfrepclf  5289  axsepgfromrep  5292  axsepg  5295  bm1.3ii  5297  axnul  5300  0ex  5302  nalset  5308  vnex  5309  axpweq  5345  pwnss  5346  zfpow  5361  axpow2  5362  axpow3  5363  elALT2  5364  dtruALT2  5365  dvdemo1  5368  dvdemo2  5369  nfnid  5370  vpwex  5372  axprlem1  5418  axprlem2  5419  axprlem4  5421  axprlem5  5422  axpr  5423  exel  5430  exexneq  5431  el  5434  sels  5435  elALT  5437  dtruOLD  5438  dfepfr  5658  epfrc  5659  wetrep  5666  wefrc  5667  rele  5824  dmep  5921  rnep  5924  ordelord  6386  onfr  6403  iotanul2  6513  funimaexgOLD  6635  zfun  7736  axun2  7737  uniex2  7738  uniuni  7759  epweon  7772  epweonALT  7773  onint  7788  omsson  7869  trom  7874  peano5  7894  frxp2  8144  frxp3  8151  poseq  8158  frrlem4  8289  frrlem8  8293  frrlem10  8295  wfrlem12OLD  8335  dfsmo2  8362  issmo  8363  smores2  8369  smo11  8379  smogt  8382  dfrecs3  8387  dfrecs3OLD  8388  tz7.48lem  8456  tz7.48-2  8457  omeulem1  8597  coflton  8686  cofon1  8687  cofonr  8689  naddcllem  8691  naddrid  8698  naddssim  8700  pw2eng  9097  infensuc  9174  findcard2d  9185  pssnn  9187  1sdomOLD  9268  unxpdomlem1  9269  unxpdomlem2  9270  unxpdomlem3  9271  pssnnOLD  9284  findcard2OLD  9303  ac6sfi  9306  frfi  9307  fissuni  9376  axreg2  9611  zfregcl  9612  epinid0  9618  cnvepnep  9626  dford2  9638  inf0  9639  inf1  9640  inf2  9641  zfinf  9657  axinf2  9658  zfinf2  9660  axinf  9662  dfom4  9667  dfom5  9668  unbnn3  9677  noinfep  9678  cantnf  9711  ttrcltr  9734  epfrs  9749  r111  9793  dif1card  10028  alephle  10106  aceq1  10135  aceq0  10136  aceq2  10137  dfac3  10139  dfac5lem2  10142  dfac5lem4  10144  dfac5  10146  dfac2a  10147  dfac2b  10148  dfac2  10149  dfac7  10150  dfac0  10151  dfac1  10152  kmlem2  10169  kmlem3  10170  kmlem4  10171  kmlem5  10172  kmlem8  10175  kmlem14  10181  kmlem15  10182  dfackm  10184  ackbij1lem10  10247  coflim  10279  cflim2  10281  cfsmolem  10288  fin23lem26  10343  ituniiun  10440  domtriomlem  10460  axdc3lem2  10469  zfac  10478  ac2  10479  ac3  10480  axac3  10482  axac2  10484  axac  10485  nd1  10605  nd2  10606  nd3  10607  nd4  10608  axextnd  10609  axrepndlem1  10610  axrepndlem2  10611  axrepnd  10612  axunndlem1  10613  axunnd  10614  axpowndlem1  10615  axpowndlem2  10616  axpowndlem3  10617  axpowndlem4  10618  axpownd  10619  axregndlem1  10620  axregndlem2  10621  axregnd  10622  axinfndlem1  10623  axinfnd  10624  axacndlem1  10625  axacndlem2  10626  axacndlem3  10627  axacndlem4  10628  axacndlem5  10629  axacnd  10630  inar1  10793  axgroth5  10842  axgroth2  10843  grothpw  10844  axgroth6  10846  grothomex  10847  axgroth3  10849  axgroth4  10850  grothprimlem  10851  grothprim  10852  inaprc  10854  nqereu  10947  npex  11004  elnpi  11006  hashbclem  14438  fsum2dlem  15743  fprod2dlem  15951  fprod2d  15952  rpnnen2  16197  lcmfunsnlem2lem2  16604  ismre  17564  fnmre  17565  mremre  17578  isacs  17625  isacs1i  17631  mreacs  17632  acsfn1  17635  acsfn2  17637  isacs3lem  18528  pmtrprfval  19436  pmtrsn  19468  gsum2dlem2  19920  lbsextlem4  21043  drngnidl  21132  mplcoe1  21969  mplcoe5  21972  selvffval  22053  selvfval  22054  mdetunilem9  22516  mdetuni0  22517  maducoeval2  22536  madugsum  22539  isbasis3g  22846  tgcl  22866  tgss2  22884  toponmre  22991  neiptopnei  23030  ist0  23218  ishaus  23220  t0top  23227  haustop  23229  isreg  23230  ist0-2  23242  ist0-3  23243  t1t0  23246  ist1-3  23247  ishaus2  23249  haust1  23250  cmpsublem  23297  cmpsub  23298  tgcmp  23299  hauscmp  23305  bwth  23308  is1stc2  23340  2ndcctbss  23353  2ndcdisj  23354  2ndcdisj2  23355  2ndcomap  23356  2ndcsep  23357  dis2ndc  23358  restnlly  23380  restlly  23381  llyidm  23386  nllyidm  23387  lly1stc  23394  finptfin  23416  locfincmp  23424  comppfsc  23430  ptpjopn  23510  tx1stc  23548  txkgen  23550  xkohaus  23551  xkococnlem  23557  xkoinjcn  23585  ist0-4  23627  kqt0lem  23634  regr1lem2  23638  kqt0  23644  r0sep  23646  nrmr0reg  23647  regr1  23648  kqreg  23649  kqnrm  23650  kqhmph  23717  isfil  23745  filuni  23783  isufil  23801  uffinfix  23825  fmfnfmlem4  23855  hauspwpwf1  23885  alexsublem  23942  alexsubALTlem3  23947  alexsubALTlem4  23948  alexsubALT  23949  ustval  24101  isust  24102  blbas  24330  met1stc  24424  metrest  24427  xrsmopn  24722  cnheibor  24875  itg2cn  25687  jensen  26915  sqff1o  27108  nosupno  27630  noinfno  27645  lrrecfr  27854  om2noseqf1o  28168  om2noseqiso  28169  dfn0s2  28195  f1otrg  28669  uhgrnbgr0nb  29161  rusgrpropedg  29392  isplig  30280  ispligb  30281  tncp  30282  l2p  30283  eulplig  30289  spanuni  31348  sumdmdii  32219  gsumvsca2  32929  nsgmgc  33117  nsgqusf1olem1  33118  nsgqusf1olem3  33120  fedgmul  33320  extdg1id  33346  indf1o  33638  gsumesum  33673  dya2iocuni  33898  bnj219  34359  bnj1098  34409  bnj594  34538  bnj580  34539  bnj601  34546  bnj849  34551  bnj996  34582  bnj1006  34586  bnj1029  34594  bnj1033  34595  bnj1090  34605  bnj1110  34608  bnj1124  34614  bnj1128  34616  fineqvrep  34710  fineqvpow  34711  erdsze  34807  connpconn  34840  rellysconn  34856  cvmsss2  34879  cvmlift2lem12  34919  axextprim  35290  axrepprim  35291  axunprim  35292  axpowprim  35293  axregprim  35294  axinfprim  35295  axacprim  35296  untelirr  35297  untuni  35298  untsucf  35299  unt0  35300  untint  35301  untangtr  35303  dftr6  35340  dffr5  35343  elpotr  35372  dfon2lem3  35376  dfon2lem4  35377  dfon2lem5  35378  dfon2lem6  35379  dfon2lem7  35380  dfon2lem8  35381  dfon2lem9  35382  dfon2  35383  axextdfeq  35388  ax8dfeq  35389  axextdist  35390  axextbdist  35391  exnel  35393  distel  35394  axextndbi  35395  dfiota3  35514  brcup  35530  brcap  35531  dfint3  35543  imagesset  35544  hftr  35773  fness  35828  fneref  35829  neibastop2lem  35839  onsuct0  35920  bj-ax89  36149  bj-elequ12  36150  bj-cleljusti  36151  bj-nfeel2  36326  bj-axc14nf  36327  bj-axc14  36328  eliminable-veqab  36338  eliminable-abeqv  36339  eliminable-abelv  36341  eliminable-abelab  36342  bj-zfauscl  36397  bj-ru0  36416  bj-ru1  36417  bj-ru  36418  currysetlem  36419  curryset  36420  currysetlem1  36421  currysetlem3  36423  currysetALT  36424  bj-abex  36504  bj-clex  36505  bj-snexg  36508  bj-axbun  36510  bj-unexg  36512  bj-axadj  36515  bj-adjg1  36517  bj-nul  36530  bj-nuliota  36531  bj-nuliotaALT  36532  bj-bm1.3ii  36538  bj-epelg  36542  finixpnum  37073  fin2solem  37074  fin2so  37075  matunitlindflem1  37084  poimirlem30  37118  poimirlem32  37120  poimir  37121  mblfinlem1  37125  mbfresfi  37134  cnambfre  37136  ftc1anc  37169  ftc2nc  37170  cover2g  37184  sstotbnd2  37242  unichnidl  37499  dfcoels  37897  dfeldisj5  38188  prtlem5  38327  prtlem12  38334  prtlem13  38335  prtlem16  38336  prtlem15  38342  prtlem17  38343  prtlem18  38344  prter1  38346  prter3  38349  ax5el  38404  dveel2ALT  38406  ax12el  38409  pclfinclN  39418  dvh1dim  40910  sn-axrep5v  41695  sn-axprlem3  41696  sn-exelALT  41697  prjspval  42018  ismrcd1  42109  dford3lem2  42439  dford4  42441  pw2f1ocnv  42449  pw2f1o2  42450  wepwsolem  42457  fnwe2lem2  42466  aomclem8  42476  kelac1  42478  pwslnm  42509  idomsubgmo  42612  uniel  42636  unielss  42637  ssunib  42639  onmaxnelsup  42642  onsupnmax  42647  onsupuni  42648  onsupmaxb  42658  onsupeqnmax  42666  oaordnr  42716  omnord1  42725  nnoeomeqom  42732  oenord1  42736  cantnfresb  42744  cantnf2  42745  oaun3lem1  42794  nadd2rabtr  42804  nadd1suc  42812  naddsuc2  42813  naddgeoa  42815  intabssd  42940  eu0  42941  ontric3g  42943  omssrncard  42961  alephiso2  42979  inintabss  42999  inintabd  43000  cnvcnvintabd  43021  elintima  43074  dffrege76  43360  frege77  43361  frege89  43373  frege90  43374  frege91  43375  frege93  43377  frege94  43378  frege95  43379  clsk1indlem3  43464  ntrneiel2  43507  ntrneik2  43513  ntrneix2  43514  ntrneik4  43522  gneispa  43551  gneispace2  43553  gneispace3  43554  gneispace  43555  gneispacef  43556  gneispacef2  43557  gneispacern2  43560  gneispace0nelrn  43561  gneispaceel  43564  gneispaceel2  43565  gneispacess  43566  ismnu  43689  mnuop123d  43690  mnussd  43691  mnuop23d  43694  mnupwd  43695  mnuop3d  43699  mnuprdlem4  43703  mnutrd  43708  grumnudlem  43713  ismnuprim  43722  rr-grothprimbi  43723  rr-grothprim  43728  ismnushort  43729  dfuniv2  43730  rr-grothshortbi  43731  rr-grothshort  43732  sbcoreleleq  43965  tratrb  43966  ordelordALT  43967  trsbc  43970  truniALT  43971  onfrALTlem5  43972  onfrALTlem4  43973  onfrALTlem3  43974  onfrALTlem2  43976  onfrALTlem1  43978  onfrALT  43979  sspwtrALT  44252  suctrALT2  44267  tratrbVD  44291  truniALTVD  44308  trintALT  44311  onfrALTlem4VD  44316  csbunigVD  44328  iota0ndef  46412  aiota0ndef  46468  ralndv1  46476  dfnelbr2  46644  nelbr  46645  nelbrim  46646  sprsymrelf1lem  46822  sprsymrelf  46826  paireqne  46842  dflinc2  47469  lcosslsp  47497  nfintd  48095
  Copyright terms: Public domain W3C validator