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  2929  sbabel  2935  sbabelOLD  2936  sbralie  3351  rru  3774  ru  3775  nfunid  4914  uniprg  4924  csbuni  4939  unissb  4942  inteq  4952  elint  4955  elintg  4957  nfint  4959  int0  4965  intss  4972  intprg  4984  dfiun2g  5033  uniiun  5061  intiin  5062  dftr2c  5268  dftr5  5269  axrep1  5286  axreplem  5287  axrep2  5288  axrep3  5289  axrep4  5290  axrep5  5291  axrep6  5292  axrep6g  5293  zfrepclf  5294  axsepgfromrep  5297  axsepg  5300  bm1.3ii  5302  axnul  5305  0ex  5307  nalset  5313  vnex  5314  inuni  5345  axpweq  5350  pwnss  5351  zfpow  5366  axpow2  5367  axpow3  5368  elALT2  5369  dtruALT2  5370  dvdemo1  5373  dvdemo2  5374  nfnid  5375  vpwex  5377  axprlem1  5423  axprlem2  5424  axprlem4  5426  axprlem5  5427  axpr  5428  exel  5435  exexneq  5436  el  5439  sels  5440  elALT  5442  dtruOLD  5443  dfepfr  5663  epfrc  5664  wetrep  5671  wefrc  5672  rele  5829  dmep  5926  rnep  5929  ordelord  6391  onfr  6408  iotanul2  6518  funimaexgOLD  6640  zfun  7741  axun2  7742  uniex2  7743  uniuni  7764  epweon  7777  epweonALT  7778  onint  7793  omsson  7874  trom  7879  peano5  7899  frxp2  8149  frxp3  8156  poseq  8163  frrlem4  8294  frrlem8  8298  frrlem10  8300  wfrlem12OLD  8340  dfsmo2  8367  issmo  8368  smores2  8374  smo11  8384  smogt  8387  dfrecs3  8392  dfrecs3OLD  8393  tz7.48lem  8461  tz7.48-2  8462  omeulem1  8602  coflton  8691  cofon1  8692  cofonr  8694  naddcllem  8696  naddrid  8703  naddssim  8705  pw2eng  9102  infensuc  9179  findcard2d  9190  pssnn  9192  1sdomOLD  9273  unxpdomlem1  9274  unxpdomlem2  9275  unxpdomlem3  9276  pssnnOLD  9289  findcard2OLD  9308  ac6sfi  9311  frfi  9312  fissuni  9381  axreg2  9616  zfregcl  9617  epinid0  9623  cnvepnep  9631  dford2  9643  inf0  9644  inf1  9645  inf2  9646  zfinf  9662  axinf2  9663  zfinf2  9665  axinf  9667  dfom4  9672  dfom5  9673  unbnn3  9682  noinfep  9683  cantnf  9716  ttrcltr  9739  epfrs  9754  r111  9798  dif1card  10033  alephle  10111  aceq1  10140  aceq0  10141  aceq2  10142  dfac3  10144  dfac5lem2  10147  dfac5lem4  10149  dfac5  10151  dfac2a  10152  dfac2b  10153  dfac2  10154  dfac7  10155  dfac0  10156  dfac1  10157  kmlem2  10174  kmlem3  10175  kmlem4  10176  kmlem5  10177  kmlem8  10180  kmlem14  10186  kmlem15  10187  dfackm  10189  ackbij1lem10  10252  coflim  10284  cflim2  10286  cfsmolem  10293  fin23lem26  10348  ituniiun  10445  domtriomlem  10465  axdc3lem2  10474  zfac  10483  ac2  10484  ac3  10485  axac3  10487  axac2  10489  axac  10490  nd1  10610  nd2  10611  nd3  10612  nd4  10613  axextnd  10614  axrepndlem1  10615  axrepndlem2  10616  axrepnd  10617  axunndlem1  10618  axunnd  10619  axpowndlem1  10620  axpowndlem2  10621  axpowndlem3  10622  axpowndlem4  10623  axpownd  10624  axregndlem1  10625  axregndlem2  10626  axregnd  10627  axinfndlem1  10628  axinfnd  10629  axacndlem1  10630  axacndlem2  10631  axacndlem3  10632  axacndlem4  10633  axacndlem5  10634  axacnd  10635  inar1  10798  axgroth5  10847  axgroth2  10848  grothpw  10849  axgroth6  10851  grothomex  10852  axgroth3  10854  axgroth4  10855  grothprimlem  10856  grothprim  10857  inaprc  10859  nqereu  10952  npex  11009  elnpi  11011  hashbclem  14443  fsum2dlem  15748  fprod2dlem  15956  fprod2d  15957  rpnnen2  16202  lcmfunsnlem2lem2  16609  ismre  17569  fnmre  17570  mremre  17583  isacs  17630  isacs1i  17636  mreacs  17637  acsfn1  17640  acsfn2  17642  isacs3lem  18533  pmtrprfval  19441  pmtrsn  19473  gsum2dlem2  19925  lbsextlem4  21048  drngnidl  21137  mplcoe1  21974  mplcoe5  21977  selvffval  22058  selvfval  22059  mdetunilem9  22521  mdetuni0  22522  maducoeval2  22541  madugsum  22544  isbasis3g  22851  tgcl  22871  tgss2  22889  toponmre  22996  neiptopnei  23035  ist0  23223  ishaus  23225  t0top  23232  haustop  23234  isreg  23235  ist0-2  23247  ist0-3  23248  t1t0  23251  ist1-3  23252  ishaus2  23254  haust1  23255  cmpsublem  23302  cmpsub  23303  tgcmp  23304  hauscmp  23310  bwth  23313  is1stc2  23345  2ndcctbss  23358  2ndcdisj  23359  2ndcdisj2  23360  2ndcomap  23361  2ndcsep  23362  dis2ndc  23363  restnlly  23385  restlly  23386  llyidm  23391  nllyidm  23392  lly1stc  23399  finptfin  23421  locfincmp  23429  comppfsc  23435  ptpjopn  23515  tx1stc  23553  txkgen  23555  xkohaus  23556  xkococnlem  23562  xkoinjcn  23590  ist0-4  23632  kqt0lem  23639  regr1lem2  23643  kqt0  23649  r0sep  23651  nrmr0reg  23652  regr1  23653  kqreg  23654  kqnrm  23655  kqhmph  23722  isfil  23750  filuni  23788  isufil  23806  uffinfix  23830  fmfnfmlem4  23860  hauspwpwf1  23890  alexsublem  23947  alexsubALTlem3  23952  alexsubALTlem4  23953  alexsubALT  23954  ustval  24106  isust  24107  blbas  24335  met1stc  24429  metrest  24432  xrsmopn  24727  cnheibor  24880  itg2cn  25692  jensen  26920  sqff1o  27113  nosupno  27635  noinfno  27650  lrrecfr  27859  om2noseqf1o  28173  om2noseqiso  28174  dfn0s2  28200  f1otrg  28674  uhgrnbgr0nb  29166  rusgrpropedg  29397  isplig  30285  ispligb  30286  tncp  30287  l2p  30288  eulplig  30294  spanuni  31353  sumdmdii  32224  gsumvsca2  32934  nsgmgc  33122  nsgqusf1olem1  33123  nsgqusf1olem3  33125  fedgmul  33325  extdg1id  33351  indf1o  33643  gsumesum  33678  dya2iocuni  33903  bnj219  34364  bnj1098  34414  bnj594  34543  bnj580  34544  bnj601  34551  bnj849  34556  bnj996  34587  bnj1006  34591  bnj1029  34599  bnj1033  34600  bnj1090  34610  bnj1110  34613  bnj1124  34619  bnj1128  34621  fineqvrep  34715  fineqvpow  34716  erdsze  34812  connpconn  34845  rellysconn  34861  cvmsss2  34884  cvmlift2lem12  34924  axextprim  35295  axrepprim  35296  axunprim  35297  axpowprim  35298  axregprim  35299  axinfprim  35300  axacprim  35301  untelirr  35302  untuni  35303  untsucf  35304  unt0  35305  untint  35306  untangtr  35308  dftr6  35345  dffr5  35348  elpotr  35377  dfon2lem3  35381  dfon2lem4  35382  dfon2lem5  35383  dfon2lem6  35384  dfon2lem7  35385  dfon2lem8  35386  dfon2lem9  35387  dfon2  35388  axextdfeq  35393  ax8dfeq  35394  axextdist  35395  axextbdist  35396  exnel  35398  distel  35399  axextndbi  35400  dfiota3  35519  brcup  35535  brcap  35536  dfint3  35548  imagesset  35549  hftr  35778  fness  35833  fneref  35834  neibastop2lem  35844  onsuct0  35925  bj-ax89  36154  bj-elequ12  36155  bj-cleljusti  36156  bj-nfeel2  36331  bj-axc14nf  36332  bj-axc14  36333  eliminable-veqab  36343  eliminable-abeqv  36344  eliminable-abelv  36346  eliminable-abelab  36347  bj-zfauscl  36402  bj-ru0  36421  bj-ru1  36422  bj-ru  36423  currysetlem  36424  curryset  36425  currysetlem1  36426  currysetlem3  36428  currysetALT  36429  bj-abex  36509  bj-clex  36510  bj-snexg  36513  bj-axbun  36515  bj-unexg  36517  bj-axadj  36520  bj-adjg1  36522  bj-nul  36535  bj-nuliota  36536  bj-nuliotaALT  36537  bj-bm1.3ii  36543  bj-epelg  36547  finixpnum  37078  fin2solem  37079  fin2so  37080  matunitlindflem1  37089  poimirlem30  37123  poimirlem32  37125  poimir  37126  mblfinlem1  37130  mbfresfi  37139  cnambfre  37141  ftc1anc  37174  ftc2nc  37175  cover2g  37189  sstotbnd2  37247  unichnidl  37504  dfcoels  37902  dfeldisj5  38193  prtlem5  38332  prtlem12  38339  prtlem13  38340  prtlem16  38341  prtlem15  38347  prtlem17  38348  prtlem18  38349  prter1  38351  prter3  38354  ax5el  38409  dveel2ALT  38411  ax12el  38414  pclfinclN  39423  dvh1dim  40915  sn-axrep5v  41704  sn-axprlem3  41705  sn-exelALT  41706  prjspval  42027  ismrcd1  42118  dford3lem2  42448  dford4  42450  pw2f1ocnv  42458  pw2f1o2  42459  wepwsolem  42466  fnwe2lem2  42475  aomclem8  42485  kelac1  42487  pwslnm  42518  idomsubgmo  42621  uniel  42645  unielss  42646  ssunib  42648  onmaxnelsup  42651  onsupnmax  42656  onsupuni  42657  onsupmaxb  42667  onsupeqnmax  42675  oaordnr  42725  omnord1  42734  nnoeomeqom  42741  oenord1  42745  cantnfresb  42753  cantnf2  42754  oaun3lem1  42803  nadd2rabtr  42813  nadd1suc  42821  naddsuc2  42822  naddgeoa  42824  intabssd  42949  eu0  42950  ontric3g  42952  omssrncard  42970  alephiso2  42988  inintabss  43008  inintabd  43009  cnvcnvintabd  43030  elintima  43083  dffrege76  43369  frege77  43370  frege89  43382  frege90  43383  frege91  43384  frege93  43386  frege94  43387  frege95  43388  clsk1indlem3  43473  ntrneiel2  43516  ntrneik2  43522  ntrneix2  43523  ntrneik4  43531  gneispa  43560  gneispace2  43562  gneispace3  43563  gneispace  43564  gneispacef  43565  gneispacef2  43566  gneispacern2  43569  gneispace0nelrn  43570  gneispaceel  43573  gneispaceel2  43574  gneispacess  43575  ismnu  43698  mnuop123d  43699  mnussd  43700  mnuop23d  43703  mnupwd  43704  mnuop3d  43708  mnuprdlem4  43712  mnutrd  43717  grumnudlem  43722  ismnuprim  43731  rr-grothprimbi  43732  rr-grothprim  43737  ismnushort  43738  dfuniv2  43739  rr-grothshortbi  43740  rr-grothshort  43741  sbcoreleleq  43974  tratrb  43975  ordelordALT  43976  trsbc  43979  truniALT  43980  onfrALTlem5  43981  onfrALTlem4  43982  onfrALTlem3  43983  onfrALTlem2  43985  onfrALTlem1  43987  onfrALT  43988  sspwtrALT  44261  suctrALT2  44276  tratrbVD  44300  truniALTVD  44317  trintALT  44320  onfrALTlem4VD  44325  csbunigVD  44337  iota0ndef  46421  aiota0ndef  46477  ralndv1  46485  dfnelbr2  46653  nelbr  46654  nelbrim  46655  sprsymrelf1lem  46831  sprsymrelf  46835  paireqne  46851  dflinc2  47478  lcosslsp  47506  nfintd  48104
  Copyright terms: Public domain W3C validator