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

Theorem wel 2140
Description: Extend wff definition to include atomic formulas with the epsilon (membership) predicate. This is read "𝑥 is an element of 𝑦," "𝑥 is a member of 𝑦," "𝑥 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 (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 2140 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 2139. This lets us avoid overloading the connective, thus preventing ambiguity that would complicate certain Metamath parsers. However, logically wel 2140 is considered to be a primitive syntax, even though here it is artificially "derived" from wcel 2139. 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 𝑥𝑦

Proof of Theorem wel
StepHypRef Expression
1 wcel 2139 1 wff 𝑥𝑦
Colors of variables: wff setvar class
Syntax hints:  wcel 2139
This theorem is referenced by:  ax8  2145  elequ1  2146  cleljust  2147  ax9  2152  elequ2  2153  ax12wdemo  2161  cleljustALT  2330  cleljustALT2  2331  dveel1  2507  dveel2  2508  axc14  2509  elsb3  2571  elsb4  2572  axext2  2741  axext3  2742  axext3ALT  2743  axext4  2744  bm1.1  2745  sbabel  2931  ru  3575  nfuni  4594  nfunid  4595  unieq  4596  csbuni  4618  inteq  4630  elintg  4635  nfint  4638  int0  4642  intss  4650  uniiun  4725  intiin  4726  trint  4920  trintssOLD  4922  axrep1  4924  axrep2  4925  axrep3  4926  axrep4  4927  axrep5  4928  zfrepclf  4929  axsep  4932  axsep2  4934  bm1.3ii  4936  zfnuleu  4938  axnul  4940  0ex  4942  nalset  4947  axpweq  4991  zfpow  4993  axpow2  4994  axpow3  4995  el  4996  dtru  5006  nfnid  5046  dvdemo1  5051  dvdemo2  5052  dfepfr  5251  wetrep  5259  wefrc  5260  rele  5406  ordelord  5906  onfr  5924  funimaexg  6136  zfun  7115  axun2  7116  uniuni  7136  onint  7160  ordom  7239  wfrlem12  7595  dfsmo2  7613  smores2  7620  smo11  7630  smogt  7633  dfrecs3  7638  tz7.48lem  7705  tz7.48-2  7706  omeulem1  7831  pw2eng  8231  infensuc  8303  1sdom  8328  unxpdomlem1  8329  unxpdomlem2  8330  unxpdomlem3  8331  pssnn  8343  findcard2  8365  findcard2d  8367  ac6sfi  8369  frfi  8370  fissuni  8436  axreg2  8663  zfregcl  8664  epinid0  8670  cnvepnep  8676  dford2  8690  inf0  8691  inf1  8692  inf2  8693  zfinf  8709  axinf2  8710  zfinf2  8712  dfom4  8719  dfom5  8720  unbnn3  8729  noinfep  8730  cantnf  8763  epfrs  8780  r111  8811  dif1card  9023  alephle  9101  aceq1  9130  aceq0  9131  aceq2  9132  dfac3  9134  dfac5lem2  9137  dfac5lem4  9139  dfac5  9141  dfac2a  9142  dfac2  9144  dfac2OLD  9145  dfac7  9146  dfac0  9147  dfac1  9148  kmlem3  9166  kmlem4  9167  kmlem5  9168  kmlem8  9171  kmlem14  9177  kmlem15  9178  dfackm  9180  ackbij1lem10  9243  coflim  9275  cflim2  9277  cfsmolem  9284  fin23lem26  9339  ituniiun  9436  domtriomlem  9456  axdc3lem2  9465  zfac  9474  ac2  9475  ac3  9476  axac3  9478  axac2  9480  axac  9481  nd1  9601  nd2  9602  nd3  9603  nd4  9604  axextnd  9605  axrepndlem1  9606  axrepndlem2  9607  axrepnd  9608  axunndlem1  9609  axunnd  9610  axpowndlem1  9611  axpowndlem2  9612  axpowndlem3  9613  axpowndlem4  9614  axpownd  9615  axregndlem1  9616  axregndlem2  9617  axregnd  9618  axinfndlem1  9619  axinfnd  9620  axacndlem1  9621  axacndlem2  9622  axacndlem3  9623  axacndlem4  9624  axacndlem5  9625  axacnd  9626  fpwwe2lem12  9655  inar1  9789  axgroth5  9838  axgroth2  9839  grothpw  9840  axgroth6  9842  grothomex  9843  axgroth3  9845  axgroth4  9846  grothprimlem  9847  grothprim  9848  nqereu  9943  npex  10000  elnpi  10002  hashbclem  13428  fsum2dlem  14700  fprod2dlem  14909  fprod2d  14910  rpnnen2  15154  lcmfunsnlem2lem2  15554  ismre  16452  fnmre  16453  mremre  16466  isacs  16513  isacs1i  16519  mreacs  16520  acsfn1  16523  acsfn2  16525  isacs3lem  17367  pmtrprfval  18107  pmtrsn  18139  gsum2dlem2  18570  lbsextlem4  19363  drngnidl  19431  mplcoe1  19667  mplcoe5  19670  mdetunilem9  20628  mdetuni0  20629  maducoeval2  20648  madugsum  20651  isbasis3g  20955  tgcl  20975  tgss2  20993  toponmre  21099  neiptopnei  21138  ist0  21326  ishaus  21328  t0top  21335  haustop  21337  isreg  21338  ist0-2  21350  ist0-3  21351  t1t0  21354  ist1-3  21355  ishaus2  21357  haust1  21358  cmpsublem  21404  cmpsub  21405  tgcmp  21406  hauscmp  21412  bwth  21415  is1stc2  21447  2ndcctbss  21460  2ndcdisj  21461  2ndcdisj2  21462  2ndcomap  21463  2ndcsep  21464  dis2ndc  21465  restnlly  21487  restlly  21488  llyidm  21493  nllyidm  21494  lly1stc  21501  finptfin  21523  locfincmp  21531  ptpjopn  21617  tx1stc  21655  txkgen  21657  xkohaus  21658  xkococnlem  21664  xkoinjcn  21692  ist0-4  21734  kqt0lem  21741  regr1lem2  21745  kqt0  21751  r0sep  21753  nrmr0reg  21754  regr1  21755  kqreg  21756  kqnrm  21757  kqhmph  21824  isfil  21852  filuni  21890  isufil  21908  uffinfix  21932  fmfnfmlem4  21962  hauspwpwf1  21992  alexsublem  22049  alexsubALTlem3  22054  alexsubALTlem4  22055  alexsubALT  22056  ustval  22207  isust  22208  blbas  22436  met1stc  22527  metrest  22530  xrsmopn  22816  cnheibor  22955  jensen  24914  sqff1o  25107  uhgrnbgr0nb  26449  rusgrpropedg  26690  isplig  27639  ispligb  27640  tncp  27641  l2p  27642  eulplig  27648  spanuni  28712  sumdmdii  29583  gsumvsca2  30092  indf1o  30395  gsumesum  30430  dya2iocuni  30654  bnj219  31108  bnj1098  31161  bnj594  31289  bnj580  31290  bnj601  31297  bnj849  31302  bnj996  31332  bnj1006  31336  bnj1029  31343  bnj1033  31344  bnj1090  31354  bnj1110  31357  bnj1124  31363  bnj1128  31365  erdsze  31491  connpconn  31524  rellysconn  31540  cvmsss2  31563  cvmlift2lem12  31603  axextprim  31885  axrepprim  31886  axunprim  31887  axpowprim  31888  axregprim  31889  axinfprim  31890  axacprim  31891  untelirr  31892  untuni  31893  untsucf  31894  unt0  31895  untint  31896  untangtr  31898  dftr6  31947  dffr5  31950  elpotr  31991  dfon2lem3  31995  dfon2lem4  31996  dfon2lem5  31997  dfon2lem6  31998  dfon2lem7  31999  dfon2lem8  32000  dfon2lem9  32001  dfon2  32002  domep  32003  axextdfeq  32008  ax8dfeq  32009  axextdist  32010  axext4dist  32011  exnel  32013  distel  32014  axextndbi  32015  poseq  32059  frrlem4  32089  frrlem11  32098  nosupno  32155  dfiota3  32336  brcup  32352  brcap  32353  dfint3  32365  imagesset  32366  hftr  32595  fness  32650  fneref  32651  neibastop2lem  32661  onsuct0  32746  bj-elequ2g  32972  bj-ax89  32973  bj-elequ12  32974  bj-cleljusti  32975  bj-axext3  33075  bj-axext4  33076  bj-clabel  33089  bj-axrep1  33094  bj-axrep2  33095  bj-axrep3  33096  bj-axrep4  33097  bj-axrep5  33098  bj-axsep  33099  bj-nalset  33100  bj-zfpow  33101  bj-el  33102  bj-dtru  33103  bj-dvdemo1  33108  bj-dvdemo2  33109  bj-nfeel2  33143  bj-axc14nf  33144  bj-axc14  33145  bj-ax8  33193  bj-dfclel  33195  bj-ax9  33196  bj-ax9-2  33197  bj-cleqhyp  33198  bj-dfcleq  33200  bj-axsep2  33227  bj-ru0  33238  bj-ru1  33239  bj-ru  33240  bj-nul  33324  bj-nuliota  33325  bj-nuliotaALT  33326  finixpnum  33707  fin2solem  33708  fin2so  33709  matunitlindflem1  33718  poimirlem30  33752  poimirlem32  33754  poimir  33755  mblfinlem1  33759  mbfresfi  33769  cnambfre  33771  ftc1anc  33806  ftc2nc  33807  cover2g  33822  sstotbnd2  33886  unichnidl  34143  prtlem5  34649  prtlem12  34656  prtlem13  34657  prtlem15  34664  prtlem17  34665  prtlem18  34666  prter1  34668  prter3  34671  ax5el  34726  dveel2ALT  34728  ax12el  34731  pclfinclN  35739  dvh1dim  37233  ismrcd1  37763  dford3lem2  38096  dford4  38098  pw2f1ocnv  38106  pw2f1o2  38107  wepwsolem  38114  fnwe2lem2  38123  aomclem8  38133  kelac1  38135  pwslnm  38166  idomsubgmo  38278  inintabss  38386  inintabd  38387  cnvcnvintabd  38408  intabssd  38418  elintima  38447  dffrege76  38735  frege77  38736  frege89  38748  frege90  38749  frege91  38750  frege93  38752  frege94  38753  frege95  38754  clsk1indlem3  38843  ntrneiel2  38886  ntrneik2  38892  ntrneix2  38893  ntrneik4  38901  gneispa  38930  gneispace2  38932  gneispace3  38933  gneispace  38934  gneispacef  38935  gneispacef2  38936  gneispacern2  38939  gneispace0nelrn  38940  gneispaceel  38943  gneispaceel2  38944  gneispacess  38945  sbcoreleleq  39247  tratrb  39248  ordelordALT  39249  trsbc  39252  truniALT  39253  onfrALTlem5  39259  onfrALTlem4  39260  onfrALTlem3  39261  onfrALTlem2  39263  onfrALTlem1  39265  onfrALT  39266  sspwtrALT  39551  suctrALT2  39571  tratrbVD  39596  truniALTVD  39613  trintALT  39616  onfrALTlem4VD  39621  dfnelbr2  41799  nelbr  41800  nelbrim  41801  sprsymrelf1lem  42251  sprsymrelf  42255  dflinc2  42709  lcosslsp  42737  nfintd  42930
  Copyright terms: Public domain W3C validator