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

Theorem wel 1977
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 1977 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 1976. This lets us avoid overloading the connective, thus preventing ambiguity that would complicate certain Metamath parsers. However, logically wel 1977 is considered to be a primitive syntax, even though here it is artificially "derived" from wcel 1976. 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 1976 1 wff 𝑥𝑦
Colors of variables: wff setvar class
Syntax hints:  wcel 1976
This theorem is referenced by:  ax8  1982  elequ1  1983  cleljust  1984  ax9  1989  elequ2  1990  ax12wdemo  1998  cleljustALT  2172  cleljustALT2  2173  dveel1  2357  dveel2  2358  axc14  2359  elsb3  2421  elsb4  2422  axext2  2590  axext3  2591  axext3ALT  2592  axext4  2593  bm1.1  2594  sbabel  2778  ru  3400  nfuni  4372  nfunid  4373  unieq  4374  csbuni  4396  inteq  4407  elintg  4412  nfint  4415  int0  4419  intss  4427  uniiun  4503  intiin  4504  trint  4690  trintss  4691  axrep1  4694  axrep2  4695  axrep3  4696  axrep4  4697  axrep5  4698  zfrepclf  4699  axsep  4702  axsep2  4704  bm1.3ii  4706  zfnuleu  4708  axnul  4710  0ex  4712  nalset  4717  axpweq  4762  zfpow  4764  axpow2  4765  axpow3  4766  el  4767  dtru  4777  nfnid  4817  dvdemo1  4823  dvdemo2  4824  dfepfr  5012  wetrep  5020  wefrc  5021  rele  5159  ordelord  5647  onfr  5665  funimaexg  5874  zfun  6825  axun2  6826  uniuni  6842  onint  6864  ordom  6943  wfrlem12  7290  dfsmo2  7308  smores2  7315  smo11  7325  smogt  7328  dfrecs3  7333  tz7.48lem  7400  tz7.48-2  7401  omeulem1  7526  pw2eng  7928  infensuc  8000  1sdom  8025  unxpdomlem1  8026  unxpdomlem2  8027  unxpdomlem3  8028  pssnn  8040  findcard2  8062  findcard2d  8064  ac6sfi  8066  frfi  8067  fissuni  8131  axreg2  8358  zfregcl  8359  zfregclOLD  8361  dford2  8377  inf0  8378  inf1  8379  inf2  8380  zfinf  8396  axinf2  8397  zfinf2  8399  dfom4  8406  dfom5  8407  unbnn3  8416  noinfep  8417  cantnf  8450  epfrs  8467  r111  8498  dif1card  8693  alephle  8771  aceq1  8800  aceq0  8801  aceq2  8802  dfac3  8804  dfac5lem2  8807  dfac5lem4  8809  dfac5  8811  dfac2a  8812  dfac2  8813  dfac7  8814  dfac0  8815  dfac1  8816  kmlem3  8834  kmlem4  8835  kmlem5  8836  kmlem8  8839  kmlem14  8845  kmlem15  8846  dfackm  8848  ackbij1lem10  8911  coflim  8943  cflim2  8945  cfsmolem  8952  fin23lem26  9007  ituniiun  9104  domtriomlem  9124  axdc3lem2  9133  zfac  9142  ac2  9143  ac3  9144  axac3  9146  axac2  9148  axac  9149  nd1  9265  nd2  9266  nd3  9267  nd4  9268  axextnd  9269  axrepndlem1  9270  axrepndlem2  9271  axrepnd  9272  axunndlem1  9273  axunnd  9274  axpowndlem1  9275  axpowndlem2  9276  axpowndlem3  9277  axpowndlem4  9278  axpownd  9279  axregndlem1  9280  axregndlem2  9281  axregnd  9282  axinfndlem1  9283  axinfnd  9284  axacndlem1  9285  axacndlem2  9286  axacndlem3  9287  axacndlem4  9288  axacndlem5  9289  axacnd  9290  fpwwe2lem12  9319  inar1  9453  axgroth5  9502  axgroth2  9503  grothpw  9504  axgroth6  9506  grothomex  9507  axgroth3  9509  axgroth4  9510  grothprimlem  9511  grothprim  9512  nqereu  9607  npex  9664  elnpi  9666  hashbclem  13047  brfi1uzindOLD  13089  brfi1indALTOLD  13091  opfi1uzindOLD  13092  fsum2dlem  14291  fprod2dlem  14497  fprod2d  14498  rpnnen2  14742  sumodd  14897  lcmfunsnlem2lem2  15138  ismre  16021  fnmre  16022  mremre  16035  isacs  16083  isacs1i  16089  mreacs  16090  acsfn1  16093  acsfn2  16095  isacs3lem  16937  pmtrprfval  17678  pmtrsn  17710  gsum2dlem2  18141  lbsextlem4  18930  drngnidl  18998  mplcoe1  19234  mplcoe5  19237  mdetunilem9  20192  mdetuni0  20193  maducoeval2  20212  madugsum  20215  isbasis3g  20511  tgcl  20531  tgss2  20549  toponmre  20654  neiptopnei  20693  ist0  20881  ishaus  20883  t0top  20890  haustop  20892  isreg  20893  ist0-2  20905  ist0-3  20906  t1t0  20909  ist1-3  20910  ishaus2  20912  haust1  20913  cmpsublem  20959  cmpsub  20960  tgcmp  20961  hauscmp  20967  bwth  20970  is1stc2  21002  2ndcctbss  21015  2ndcdisj  21016  2ndcdisj2  21017  2ndcomap  21018  2ndcsep  21019  dis2ndc  21020  restnlly  21042  restlly  21043  llyidm  21048  nllyidm  21049  lly1stc  21056  finptfin  21078  locfincmp  21086  ptpjopn  21172  tx1stc  21210  txkgen  21212  xkohaus  21213  xkococnlem  21219  xkoinjcn  21247  ist0-4  21289  kqt0lem  21296  regr1lem2  21300  kqt0  21306  r0sep  21308  nrmr0reg  21309  regr1  21310  kqreg  21311  kqnrm  21312  kqhmph  21379  isfil  21408  filuni  21446  isufil  21464  uffinfix  21488  fmfnfmlem4  21518  hauspwpwf1  21548  alexsublem  21605  alexsubALTlem3  21610  alexsubALTlem4  21611  alexsubALT  21612  ustval  21763  isust  21764  blbas  21992  met1stc  22083  metrest  22086  xrsmopn  22370  cnheibor  22509  jensen  24459  sqff1o  24652  usgrafis  25737  dfconngra1  25992  0egra0rgra  26256  isplig  26513  tncp  26514  spanuni  27580  sumdmdii  28451  gsumvsca2  28907  indf1o  29206  gsumesum  29241  dya2iocuni  29465  bnj219  29848  bnj1098  29901  bnj594  30029  bnj580  30030  bnj601  30037  bnj849  30042  bnj996  30072  bnj1006  30076  bnj1029  30083  bnj1033  30084  bnj1090  30094  bnj1110  30097  bnj1124  30103  bnj1128  30105  erdsze  30231  conpcon  30264  rellyscon  30280  cvmsss2  30303  cvmlift2lem12  30343  axextprim  30625  axrepprim  30626  axunprim  30627  axpowprim  30628  axregprim  30629  axinfprim  30630  axacprim  30631  untelirr  30632  untuni  30633  untsucf  30634  unt0  30635  untint  30636  untangtr  30638  dftr6  30686  dffr5  30689  elpotr  30723  dfon2lem3  30727  dfon2lem4  30728  dfon2lem5  30729  dfon2lem6  30730  dfon2lem7  30731  dfon2lem8  30732  dfon2lem9  30733  dfon2  30734  domep  30735  axextdfeq  30740  ax8dfeq  30741  axextdist  30742  axext4dist  30743  exnel  30745  distel  30746  axextndbi  30747  poseq  30787  frrlem11  30829  nobndlem6  30889  nofulllem5  30898  dfiota3  30993  brcup  31009  brcap  31010  dfint3  31022  imagesset  31023  hftr  31252  fness  31307  fneref  31308  neibastop2lem  31318  onsuct0  31403  bj-elequ2g  31646  bj-ax89  31647  bj-elequ12  31648  bj-cleljusti  31649  bj-axext3  31750  bj-axext4  31751  bj-clabel  31764  bj-axrep1  31769  bj-axrep2  31770  bj-axrep3  31771  bj-axrep4  31772  bj-axrep5  31773  bj-axsep  31774  bj-nalset  31775  bj-zfpow  31776  bj-el  31777  bj-dtru  31778  bj-dvdemo1  31783  bj-dvdemo2  31784  bj-ax8  31863  bj-ax9  31866  bj-cleqhyp  31867  bj-axsep2  31896  bj-ru0  31907  bj-ru1  31908  bj-ru  31909  bj-nul  31992  bj-nuliota  31993  bj-nuliotaALT  31994  bj-xnex  32028  finixpnum  32347  fin2solem  32348  fin2so  32349  matunitlindflem1  32358  poimirlem30  32392  poimirlem32  32394  poimir  32395  mblfinlem1  32399  mbfresfi  32409  cnambfre  32411  ftc1anc  32446  ftc2nc  32447  cover2g  32462  sstotbnd2  32526  unichnidl  32783  prtlem5  32945  prtlem12  32953  prtlem13  32954  prtlem15  32961  prtlem17  32962  prtlem18  32963  prter1  32965  prter3  32968  ax5el  33023  dveel2ALT  33025  ax12el  33028  pclfinclN  34037  dvh1dim  35532  ismrcd1  36062  dford3lem2  36395  dford4  36397  pw2f1ocnv  36405  pw2f1o2  36406  wepwsolem  36413  fnwe2lem2  36422  aomclem8  36432  kelac1  36434  pwslnm  36465  idomsubgmo  36578  inintabss  36686  inintabd  36687  cnvcnvintabd  36708  intabssd  36718  elintima  36747  dffrege76  37036  frege77  37037  frege89  37049  frege90  37050  frege91  37051  frege93  37053  frege94  37054  frege95  37055  clsk1indlem3  37144  ntrneiel2  37187  ntrneik2  37193  ntrneix2  37194  ntrneik4  37202  gneispa  37231  gneispace2  37233  gneispace3  37234  gneispace  37235  gneispacef  37236  gneispacef2  37237  gneispacern2  37240  gneispace0nelrn  37241  gneispaceel  37244  gneispaceel2  37245  gneispacess  37246  sbcoreleleq  37549  tratrb  37550  ordelordALT  37551  trsbc  37554  truniALT  37555  onfrALTlem5  37561  onfrALTlem4  37562  onfrALTlem3  37563  onfrALTlem2  37565  onfrALTlem1  37567  onfrALT  37568  sspwtrALT  37854  suctrALT2  37877  tratrbVD  37902  truniALTVD  37919  trintALT  37922  onfrALTlem4VD  37927  uhgrnbgr0nb  40557  rusgrpropedg  40765  dflinc2  41974  lcosslsp  42002
  Copyright terms: Public domain W3C validator