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

Theorem wel 2108
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 2108 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 2107. This lets us avoid overloading the connective, thus preventing ambiguity that would complicate certain Metamath parsers. However, logically wel 2108 is considered to be a primitive syntax, even though here it is artificially "derived" from wcel 2107. 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 2107 1 wff 𝑥𝑦
Colors of variables: wff setvar class
Syntax hints:  wcel 2107
This theorem is referenced by:  ax8  2113  elequ1  2114  elsb1  2115  cleljust  2116  ax9  2121  elequ2  2122  elequ2g  2123  elsb2  2124  ax12wdemo  2132  cleljustALT  2361  cleljustALT2  2362  dveel1  2460  dveel2  2461  axc14  2462  axexte  2709  axextg  2710  axextb  2711  axextmo  2712  nulmo  2713  cvjust  2731  ax9ALT  2732  nfcvf  2937  sbabel  2942  sbabelOLD  2943  rru  3742  ru  3743  nfunid  4876  unieqOLD  4882  uniprg  4887  csbuni  4902  unissb  4905  inteq  4915  elint  4918  elintg  4920  nfint  4922  int0  4928  intss  4935  intprg  4947  dfiun2g  4995  uniiun  5023  intiin  5024  dftr2c  5230  dftr5  5231  axrep1  5248  axreplem  5249  axrep2  5250  axrep3  5251  axrep4  5252  axrep5  5253  axrep6  5254  axrep6g  5255  zfrepclf  5256  axsepgfromrep  5259  axsepg  5262  bm1.3ii  5264  axnul  5267  0ex  5269  nalset  5275  vnex  5276  axpweq  5310  pwnss  5311  zfpow  5326  axpow2  5327  axpow3  5328  elALT2  5329  dtruALT2  5330  dvdemo1  5333  dvdemo2  5334  nfnid  5335  vpwex  5337  axprlem1  5383  axprlem2  5384  axprlem4  5386  axprlem5  5387  axpr  5388  exel  5395  exexneq  5396  el  5399  sels  5400  elALT  5402  dtruOLD  5403  dfepfr  5623  epfrc  5624  wetrep  5631  wefrc  5632  rele  5788  dmep  5884  rnep  5887  ordelord  6344  onfr  6361  iotanul2  6471  funimaexgOLD  6593  zfun  7678  axun2  7679  uniex2  7680  uniuni  7701  epweon  7714  epweonALT  7715  onint  7730  omsson  7811  trom  7816  peano5  7835  frxp2  8081  frxp3  8088  poseq  8095  frrlem4  8225  frrlem8  8229  frrlem10  8231  wfrlem12OLD  8271  dfsmo2  8298  issmo  8299  smores2  8305  smo11  8315  smogt  8318  dfrecs3  8323  dfrecs3OLD  8324  tz7.48lem  8392  tz7.48-2  8393  omeulem1  8534  coflton  8622  cofon1  8623  cofonr  8625  naddcllem  8627  naddid1  8634  naddssim  8636  pw2eng  9029  infensuc  9106  findcard2d  9117  pssnn  9119  1sdomOLD  9200  unxpdomlem1  9201  unxpdomlem2  9202  unxpdomlem3  9203  pssnnOLD  9216  findcard2OLD  9235  ac6sfi  9238  frfi  9239  fissuni  9308  axreg2  9536  zfregcl  9537  epinid0  9543  cnvepnep  9551  dford2  9563  inf0  9564  inf1  9565  inf2  9566  zfinf  9582  axinf2  9583  zfinf2  9585  axinf  9587  dfom4  9592  dfom5  9593  unbnn3  9602  noinfep  9603  cantnf  9636  ttrcltr  9659  epfrs  9674  r111  9718  dif1card  9953  alephle  10031  aceq1  10060  aceq0  10061  aceq2  10062  dfac3  10064  dfac5lem2  10067  dfac5lem4  10069  dfac5  10071  dfac2a  10072  dfac2b  10073  dfac2  10074  dfac7  10075  dfac0  10076  dfac1  10077  kmlem2  10094  kmlem3  10095  kmlem4  10096  kmlem5  10097  kmlem8  10100  kmlem14  10106  kmlem15  10107  dfackm  10109  ackbij1lem10  10172  coflim  10204  cflim2  10206  cfsmolem  10213  fin23lem26  10268  ituniiun  10365  domtriomlem  10385  axdc3lem2  10394  zfac  10403  ac2  10404  ac3  10405  axac3  10407  axac2  10409  axac  10410  nd1  10530  nd2  10531  nd3  10532  nd4  10533  axextnd  10534  axrepndlem1  10535  axrepndlem2  10536  axrepnd  10537  axunndlem1  10538  axunnd  10539  axpowndlem1  10540  axpowndlem2  10541  axpowndlem3  10542  axpowndlem4  10543  axpownd  10544  axregndlem1  10545  axregndlem2  10546  axregnd  10547  axinfndlem1  10548  axinfnd  10549  axacndlem1  10550  axacndlem2  10551  axacndlem3  10552  axacndlem4  10553  axacndlem5  10554  axacnd  10555  inar1  10718  axgroth5  10767  axgroth2  10768  grothpw  10769  axgroth6  10771  grothomex  10772  axgroth3  10774  axgroth4  10775  grothprimlem  10776  grothprim  10777  inaprc  10779  nqereu  10872  npex  10929  elnpi  10931  hashbclem  14356  fsum2dlem  15662  fprod2dlem  15870  fprod2d  15871  rpnnen2  16115  lcmfunsnlem2lem2  16522  ismre  17477  fnmre  17478  mremre  17491  isacs  17538  isacs1i  17544  mreacs  17545  acsfn1  17548  acsfn2  17550  isacs3lem  18438  pmtrprfval  19276  pmtrsn  19308  gsum2dlem2  19755  lbsextlem4  20638  drngnidl  20715  mplcoe1  21454  mplcoe5  21457  selvffval  21542  selvfval  21543  mdetunilem9  21985  mdetuni0  21986  maducoeval2  22005  madugsum  22008  isbasis3g  22315  tgcl  22335  tgss2  22353  toponmre  22460  neiptopnei  22499  ist0  22687  ishaus  22689  t0top  22696  haustop  22698  isreg  22699  ist0-2  22711  ist0-3  22712  t1t0  22715  ist1-3  22716  ishaus2  22718  haust1  22719  cmpsublem  22766  cmpsub  22767  tgcmp  22768  hauscmp  22774  bwth  22777  is1stc2  22809  2ndcctbss  22822  2ndcdisj  22823  2ndcdisj2  22824  2ndcomap  22825  2ndcsep  22826  dis2ndc  22827  restnlly  22849  restlly  22850  llyidm  22855  nllyidm  22856  lly1stc  22863  finptfin  22885  locfincmp  22893  comppfsc  22899  ptpjopn  22979  tx1stc  23017  txkgen  23019  xkohaus  23020  xkococnlem  23026  xkoinjcn  23054  ist0-4  23096  kqt0lem  23103  regr1lem2  23107  kqt0  23113  r0sep  23115  nrmr0reg  23116  regr1  23117  kqreg  23118  kqnrm  23119  kqhmph  23186  isfil  23214  filuni  23252  isufil  23270  uffinfix  23294  fmfnfmlem4  23324  hauspwpwf1  23354  alexsublem  23411  alexsubALTlem3  23416  alexsubALTlem4  23417  alexsubALT  23418  ustval  23570  isust  23571  blbas  23799  met1stc  23893  metrest  23896  xrsmopn  24191  cnheibor  24334  itg2cn  25144  jensen  26354  sqff1o  26547  nosupno  27067  noinfno  27082  lrrecfr  27277  f1otrg  27855  uhgrnbgr0nb  28344  rusgrpropedg  28574  isplig  29460  ispligb  29461  tncp  29462  l2p  29463  eulplig  29469  spanuni  30528  sumdmdii  31399  gsumvsca2  32104  nsgmgc  32230  nsgqusf1olem1  32231  nsgqusf1olem3  32233  fedgmul  32366  extdg1id  32392  indf1o  32663  gsumesum  32698  dya2iocuni  32923  bnj219  33385  bnj1098  33435  bnj594  33564  bnj580  33565  bnj601  33572  bnj849  33577  bnj996  33608  bnj1006  33612  bnj1029  33620  bnj1033  33621  bnj1090  33631  bnj1110  33634  bnj1124  33640  bnj1128  33642  fineqvrep  33736  fineqvpow  33737  erdsze  33836  connpconn  33869  rellysconn  33885  cvmsss2  33908  cvmlift2lem12  33948  axextprim  34312  axrepprim  34313  axunprim  34314  axpowprim  34315  axregprim  34316  axinfprim  34317  axacprim  34318  untelirr  34319  untuni  34320  untsucf  34321  unt0  34322  untint  34323  untangtr  34325  dftr6  34363  dffr5  34366  elpotr  34395  dfon2lem3  34399  dfon2lem4  34400  dfon2lem5  34401  dfon2lem6  34402  dfon2lem7  34403  dfon2lem8  34404  dfon2lem9  34405  dfon2  34406  axextdfeq  34411  ax8dfeq  34412  axextdist  34413  axextbdist  34414  exnel  34416  distel  34417  axextndbi  34418  dfiota3  34537  brcup  34553  brcap  34554  dfint3  34566  imagesset  34567  hftr  34796  fness  34850  fneref  34851  neibastop2lem  34861  onsuct0  34942  bj-ax89  35171  bj-elequ12  35172  bj-cleljusti  35173  bj-nfeel2  35349  bj-axc14nf  35350  bj-axc14  35351  eliminable-veqab  35361  eliminable-abeqv  35362  eliminable-abelv  35364  eliminable-abelab  35365  bj-zfauscl  35423  bj-ru0  35442  bj-ru1  35443  bj-ru  35444  currysetlem  35445  curryset  35446  currysetlem1  35447  currysetlem3  35449  currysetALT  35450  bj-abex  35530  bj-clex  35531  bj-snexg  35534  bj-axbun  35536  bj-unexg  35538  bj-axadj  35541  bj-adjg1  35543  bj-nul  35556  bj-nuliota  35557  bj-nuliotaALT  35558  bj-bm1.3ii  35564  bj-epelg  35568  finixpnum  36092  fin2solem  36093  fin2so  36094  matunitlindflem1  36103  poimirlem30  36137  poimirlem32  36139  poimir  36140  mblfinlem1  36144  mbfresfi  36153  cnambfre  36155  ftc1anc  36188  ftc2nc  36189  cover2g  36203  sstotbnd2  36262  unichnidl  36519  dfcoels  36921  dfeldisj5  37212  prtlem5  37351  prtlem12  37358  prtlem13  37359  prtlem16  37360  prtlem15  37366  prtlem17  37367  prtlem18  37368  prter1  37370  prter3  37373  ax5el  37428  dveel2ALT  37430  ax12el  37433  pclfinclN  38442  dvh1dim  39934  sn-axrep5v  40667  sn-axprlem3  40668  sn-exelALT  40669  prjspval  40970  ismrcd1  41050  dford3lem2  41380  dford4  41382  pw2f1ocnv  41390  pw2f1o2  41391  wepwsolem  41398  fnwe2lem2  41407  aomclem8  41417  kelac1  41419  pwslnm  41450  idomsubgmo  41554  uniel  41580  unielss  41581  ssunib  41583  onmaxnelsup  41586  onsupnmax  41591  onsupuni  41592  onsupmaxb  41602  onsupeqnmax  41610  oaordnr  41660  omnord1  41669  nnoeomeqom  41676  oenord1  41680  cantnfresb  41688  cantnf2  41689  oaun3lem1  41719  nadd2rabtr  41729  nadd1suc  41737  naddsuc2  41738  naddgeoa  41740  intabssd  41865  eu0  41866  ontric3g  41868  omssrncard  41886  alephiso2  41904  inintabss  41924  inintabd  41925  cnvcnvintabd  41946  elintima  41999  dffrege76  42285  frege77  42286  frege89  42298  frege90  42299  frege91  42300  frege93  42302  frege94  42303  frege95  42304  clsk1indlem3  42389  ntrneiel2  42432  ntrneik2  42438  ntrneix2  42439  ntrneik4  42447  gneispa  42476  gneispace2  42478  gneispace3  42479  gneispace  42480  gneispacef  42481  gneispacef2  42482  gneispacern2  42485  gneispace0nelrn  42486  gneispaceel  42489  gneispaceel2  42490  gneispacess  42491  ismnu  42615  mnuop123d  42616  mnussd  42617  mnuop23d  42620  mnupwd  42621  mnuop3d  42625  mnuprdlem4  42629  mnutrd  42634  grumnudlem  42639  ismnuprim  42648  rr-grothprimbi  42649  rr-grothprim  42654  ismnushort  42655  dfuniv2  42656  rr-grothshortbi  42657  rr-grothshort  42658  sbcoreleleq  42891  tratrb  42892  ordelordALT  42893  trsbc  42896  truniALT  42897  onfrALTlem5  42898  onfrALTlem4  42899  onfrALTlem3  42900  onfrALTlem2  42902  onfrALTlem1  42904  onfrALT  42905  sspwtrALT  43178  suctrALT2  43193  tratrbVD  43217  truniALTVD  43234  trintALT  43237  onfrALTlem4VD  43242  iota0ndef  45347  aiota0ndef  45403  ralndv1  45411  dfnelbr2  45579  nelbr  45580  nelbrim  45581  sprsymrelf1lem  45757  sprsymrelf  45761  paireqne  45777  dflinc2  46565  lcosslsp  46593  nfintd  47192
  Copyright terms: Public domain W3C validator