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

Theorem wel 1978
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 1978 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 1977. This lets us avoid overloading the connective, thus preventing ambiguity that would complicate certain Metamath parsers. However, logically wel 1978 is considered to be a primitive syntax, even though here it is artificially "derived" from wcel 1977. 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 1977 1 wff 𝑥𝑦
Colors of variables: wff setvar class
Syntax hints:  wcel 1977
This theorem is referenced by:  ax8  1983  elequ1  1984  cleljust  1985  ax9  1990  elequ2  1991  ax12wdemo  1999  cleljustALT  2173  cleljustALT2  2174  dveel1  2358  dveel2  2359  axc14  2360  elsb3  2422  elsb4  2423  axext2  2591  axext3  2592  axext3ALT  2593  axext4  2594  bm1.1  2595  sbabel  2779  ru  3401  nfuni  4378  nfunid  4379  unieq  4380  csbuni  4402  inteq  4413  elintg  4418  nfint  4421  int0  4425  intss  4433  uniiun  4509  intiin  4510  trint  4696  trintss  4697  axrep1  4700  axrep2  4701  axrep3  4702  axrep4  4703  axrep5  4704  zfrepclf  4705  axsep  4708  axsep2  4710  bm1.3ii  4712  zfnuleu  4714  axnul  4716  0ex  4718  nalset  4723  axpweq  4768  zfpow  4770  axpow2  4771  axpow3  4772  el  4773  dtru  4783  nfnid  4823  dvdemo1  4829  dvdemo2  4830  dfepfr  5023  wetrep  5031  wefrc  5032  rele  5172  ordelord  5662  onfr  5680  funimaexg  5889  zfun  6848  axun2  6849  uniuni  6865  onint  6887  ordom  6966  wfrlem12  7313  dfsmo2  7331  smores2  7338  smo11  7348  smogt  7351  dfrecs3  7356  tz7.48lem  7423  tz7.48-2  7424  omeulem1  7549  pw2eng  7951  infensuc  8023  1sdom  8048  unxpdomlem1  8049  unxpdomlem2  8050  unxpdomlem3  8051  pssnn  8063  findcard2  8085  findcard2d  8087  ac6sfi  8089  frfi  8090  fissuni  8154  axreg2  8381  zfregcl  8382  zfregclOLD  8384  dford2  8400  inf0  8401  inf1  8402  inf2  8403  zfinf  8419  axinf2  8420  zfinf2  8422  dfom4  8429  dfom5  8430  unbnn3  8439  noinfep  8440  cantnf  8473  epfrs  8490  r111  8521  dif1card  8716  alephle  8794  aceq1  8823  aceq0  8824  aceq2  8825  dfac3  8827  dfac5lem2  8830  dfac5lem4  8832  dfac5  8834  dfac2a  8835  dfac2  8836  dfac7  8837  dfac0  8838  dfac1  8839  kmlem3  8857  kmlem4  8858  kmlem5  8859  kmlem8  8862  kmlem14  8868  kmlem15  8869  dfackm  8871  ackbij1lem10  8934  coflim  8966  cflim2  8968  cfsmolem  8975  fin23lem26  9030  ituniiun  9127  domtriomlem  9147  axdc3lem2  9156  zfac  9165  ac2  9166  ac3  9167  axac3  9169  axac2  9171  axac  9172  nd1  9288  nd2  9289  nd3  9290  nd4  9291  axextnd  9292  axrepndlem1  9293  axrepndlem2  9294  axrepnd  9295  axunndlem1  9296  axunnd  9297  axpowndlem1  9298  axpowndlem2  9299  axpowndlem3  9300  axpowndlem4  9301  axpownd  9302  axregndlem1  9303  axregndlem2  9304  axregnd  9305  axinfndlem1  9306  axinfnd  9307  axacndlem1  9308  axacndlem2  9309  axacndlem3  9310  axacndlem4  9311  axacndlem5  9312  axacnd  9313  fpwwe2lem12  9342  inar1  9476  axgroth5  9525  axgroth2  9526  grothpw  9527  axgroth6  9529  grothomex  9530  axgroth3  9532  axgroth4  9533  grothprimlem  9534  grothprim  9535  nqereu  9630  npex  9687  elnpi  9689  hashbclem  13093  brfi1uzindOLD  13141  brfi1indALTOLD  13143  opfi1uzindOLD  13144  fsum2dlem  14343  fprod2dlem  14549  fprod2d  14550  rpnnen2  14794  sumodd  14949  lcmfunsnlem2lem2  15190  ismre  16073  fnmre  16074  mremre  16087  isacs  16135  isacs1i  16141  mreacs  16142  acsfn1  16145  acsfn2  16147  isacs3lem  16989  pmtrprfval  17730  pmtrsn  17762  gsum2dlem2  18193  lbsextlem4  18982  drngnidl  19050  mplcoe1  19286  mplcoe5  19289  mdetunilem9  20245  mdetuni0  20246  maducoeval2  20265  madugsum  20268  isbasis3g  20564  tgcl  20584  tgss2  20602  toponmre  20707  neiptopnei  20746  ist0  20934  ishaus  20936  t0top  20943  haustop  20945  isreg  20946  ist0-2  20958  ist0-3  20959  t1t0  20962  ist1-3  20963  ishaus2  20965  haust1  20966  cmpsublem  21012  cmpsub  21013  tgcmp  21014  hauscmp  21020  bwth  21023  is1stc2  21055  2ndcctbss  21068  2ndcdisj  21069  2ndcdisj2  21070  2ndcomap  21071  2ndcsep  21072  dis2ndc  21073  restnlly  21095  restlly  21096  llyidm  21101  nllyidm  21102  lly1stc  21109  finptfin  21131  locfincmp  21139  ptpjopn  21225  tx1stc  21263  txkgen  21265  xkohaus  21266  xkococnlem  21272  xkoinjcn  21300  ist0-4  21342  kqt0lem  21349  regr1lem2  21353  kqt0  21359  r0sep  21361  nrmr0reg  21362  regr1  21363  kqreg  21364  kqnrm  21365  kqhmph  21432  isfil  21461  filuni  21499  isufil  21517  uffinfix  21541  fmfnfmlem4  21571  hauspwpwf1  21601  alexsublem  21658  alexsubALTlem3  21663  alexsubALTlem4  21664  alexsubALT  21665  ustval  21816  isust  21817  blbas  22045  met1stc  22136  metrest  22139  xrsmopn  22423  cnheibor  22562  jensen  24515  sqff1o  24708  usgrafis  25944  dfconngra1  26199  0egra0rgra  26463  isplig  26720  tncp  26721  spanuni  27787  sumdmdii  28658  gsumvsca2  29114  indf1o  29413  gsumesum  29448  dya2iocuni  29672  bnj219  30055  bnj1098  30108  bnj594  30236  bnj580  30237  bnj601  30244  bnj849  30249  bnj996  30279  bnj1006  30283  bnj1029  30290  bnj1033  30291  bnj1090  30301  bnj1110  30304  bnj1124  30310  bnj1128  30312  erdsze  30438  conpcon  30471  rellyscon  30487  cvmsss2  30510  cvmlift2lem12  30550  axextprim  30832  axrepprim  30833  axunprim  30834  axpowprim  30835  axregprim  30836  axinfprim  30837  axacprim  30838  untelirr  30839  untuni  30840  untsucf  30841  unt0  30842  untint  30843  untangtr  30845  dftr6  30893  dffr5  30896  elpotr  30930  dfon2lem3  30934  dfon2lem4  30935  dfon2lem5  30936  dfon2lem6  30937  dfon2lem7  30938  dfon2lem8  30939  dfon2lem9  30940  dfon2  30941  domep  30942  axextdfeq  30947  ax8dfeq  30948  axextdist  30949  axext4dist  30950  exnel  30952  distel  30953  axextndbi  30954  poseq  30994  frrlem11  31036  nobndlem6  31096  nofulllem5  31105  dfiota3  31200  brcup  31216  brcap  31217  dfint3  31229  imagesset  31230  hftr  31459  fness  31514  fneref  31515  neibastop2lem  31525  onsuct0  31610  bj-elequ2g  31853  bj-ax89  31854  bj-elequ12  31855  bj-cleljusti  31856  bj-axext3  31957  bj-axext4  31958  bj-clabel  31971  bj-axrep1  31976  bj-axrep2  31977  bj-axrep3  31978  bj-axrep4  31979  bj-axrep5  31980  bj-axsep  31981  bj-nalset  31982  bj-zfpow  31983  bj-el  31984  bj-dtru  31985  bj-dvdemo1  31990  bj-dvdemo2  31991  bj-nfeel2  32030  bj-axc14nf  32031  bj-axc14  32032  bj-ax8  32080  bj-ax9  32083  bj-cleqhyp  32084  bj-axsep2  32113  bj-ru0  32124  bj-ru1  32125  bj-ru  32126  bj-nul  32209  bj-nuliota  32210  bj-nuliotaALT  32211  bj-xnex  32245  finixpnum  32564  fin2solem  32565  fin2so  32566  matunitlindflem1  32575  poimirlem30  32609  poimirlem32  32611  poimir  32612  mblfinlem1  32616  mbfresfi  32626  cnambfre  32628  ftc1anc  32663  ftc2nc  32664  cover2g  32679  sstotbnd2  32743  unichnidl  33000  prtlem5  33162  prtlem12  33170  prtlem13  33171  prtlem15  33178  prtlem17  33179  prtlem18  33180  prter1  33182  prter3  33185  ax5el  33240  dveel2ALT  33242  ax12el  33245  pclfinclN  34254  dvh1dim  35749  ismrcd1  36279  dford3lem2  36612  dford4  36614  pw2f1ocnv  36622  pw2f1o2  36623  wepwsolem  36630  fnwe2lem2  36639  aomclem8  36649  kelac1  36651  pwslnm  36682  idomsubgmo  36795  inintabss  36903  inintabd  36904  cnvcnvintabd  36925  intabssd  36935  elintima  36964  dffrege76  37253  frege77  37254  frege89  37266  frege90  37267  frege91  37268  frege93  37270  frege94  37271  frege95  37272  clsk1indlem3  37361  ntrneiel2  37404  ntrneik2  37410  ntrneix2  37411  ntrneik4  37419  gneispa  37448  gneispace2  37450  gneispace3  37451  gneispace  37452  gneispacef  37453  gneispacef2  37454  gneispacern2  37457  gneispace0nelrn  37458  gneispaceel  37461  gneispaceel2  37462  gneispacess  37463  sbcoreleleq  37766  tratrb  37767  ordelordALT  37768  trsbc  37771  truniALT  37772  onfrALTlem5  37778  onfrALTlem4  37779  onfrALTlem3  37780  onfrALTlem2  37782  onfrALTlem1  37784  onfrALT  37785  sspwtrALT  38071  suctrALT2  38094  tratrbVD  38119  truniALTVD  38136  trintALT  38139  onfrALTlem4VD  38144  uhgrnbgr0nb  40576  rusgrpropedg  40784  dflinc2  41993  lcosslsp  42021  nfintd  42218
  Copyright terms: Public domain W3C validator