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

Theorem wel 1988
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 1988 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 1987. This lets us avoid overloading the connective, thus preventing ambiguity that would complicate certain Metamath parsers. However, logically wel 1988 is considered to be a primitive syntax, even though here it is artificially "derived" from wcel 1987. 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 1987 1 wff 𝑥𝑦
Colors of variables: wff setvar class
Syntax hints:  wcel 1987
This theorem is referenced by:  ax8  1993  elequ1  1994  cleljust  1995  ax9  2000  elequ2  2001  ax12wdemo  2009  cleljustALT  2184  cleljustALT2  2185  dveel1  2369  dveel2  2370  axc14  2371  elsb3  2433  elsb4  2434  axext2  2602  axext3  2603  axext3ALT  2604  axext4  2605  bm1.1  2606  sbabel  2789  ru  3421  nfuni  4415  nfunid  4416  unieq  4417  csbuni  4439  inteq  4450  elintg  4455  nfint  4458  int0  4462  intss  4470  uniiun  4546  intiin  4547  trint  4738  trintssOLD  4740  axrep1  4742  axrep2  4743  axrep3  4744  axrep4  4745  axrep5  4746  zfrepclf  4747  axsep  4750  axsep2  4752  bm1.3ii  4754  zfnuleu  4756  axnul  4758  0ex  4760  nalset  4765  axpweq  4812  zfpow  4814  axpow2  4815  axpow3  4816  el  4817  dtru  4827  nfnid  4867  dvdemo1  4873  dvdemo2  4874  dfepfr  5069  wetrep  5077  wefrc  5078  rele  5220  ordelord  5714  onfr  5732  funimaexg  5943  zfun  6915  axun2  6916  abnex  6929  uniuni  6935  onint  6957  ordom  7036  wfrlem12  7386  dfsmo2  7404  smores2  7411  smo11  7421  smogt  7424  dfrecs3  7429  tz7.48lem  7496  tz7.48-2  7497  omeulem1  7622  pw2eng  8026  infensuc  8098  1sdom  8123  unxpdomlem1  8124  unxpdomlem2  8125  unxpdomlem3  8126  pssnn  8138  findcard2  8160  findcard2d  8162  ac6sfi  8164  frfi  8165  fissuni  8231  axreg2  8458  zfregcl  8459  zfregclOLD  8461  dford2  8477  inf0  8478  inf1  8479  inf2  8480  zfinf  8496  axinf2  8497  zfinf2  8499  dfom4  8506  dfom5  8507  unbnn3  8516  noinfep  8517  cantnf  8550  epfrs  8567  r111  8598  dif1card  8793  alephle  8871  aceq1  8900  aceq0  8901  aceq2  8902  dfac3  8904  dfac5lem2  8907  dfac5lem4  8909  dfac5  8911  dfac2a  8912  dfac2  8913  dfac7  8914  dfac0  8915  dfac1  8916  kmlem3  8934  kmlem4  8935  kmlem5  8936  kmlem8  8939  kmlem14  8945  kmlem15  8946  dfackm  8948  ackbij1lem10  9011  coflim  9043  cflim2  9045  cfsmolem  9052  fin23lem26  9107  ituniiun  9204  domtriomlem  9224  axdc3lem2  9233  zfac  9242  ac2  9243  ac3  9244  axac3  9246  axac2  9248  axac  9249  nd1  9369  nd2  9370  nd3  9371  nd4  9372  axextnd  9373  axrepndlem1  9374  axrepndlem2  9375  axrepnd  9376  axunndlem1  9377  axunnd  9378  axpowndlem1  9379  axpowndlem2  9380  axpowndlem3  9381  axpowndlem4  9382  axpownd  9383  axregndlem1  9384  axregndlem2  9385  axregnd  9386  axinfndlem1  9387  axinfnd  9388  axacndlem1  9389  axacndlem2  9390  axacndlem3  9391  axacndlem4  9392  axacndlem5  9393  axacnd  9394  fpwwe2lem12  9423  inar1  9557  axgroth5  9606  axgroth2  9607  grothpw  9608  axgroth6  9610  grothomex  9611  axgroth3  9613  axgroth4  9614  grothprimlem  9615  grothprim  9616  nqereu  9711  npex  9768  elnpi  9770  hashbclem  13190  brfi1uzindOLD  13241  brfi1indALTOLD  13243  opfi1uzindOLD  13244  fsum2dlem  14448  fprod2dlem  14654  fprod2d  14655  rpnnen2  14899  sumodd  15054  lcmfunsnlem2lem2  15295  ismre  16190  fnmre  16191  mremre  16204  isacs  16252  isacs1i  16258  mreacs  16259  acsfn1  16262  acsfn2  16264  isacs3lem  17106  pmtrprfval  17847  pmtrsn  17879  gsum2dlem2  18310  lbsextlem4  19101  drngnidl  19169  mplcoe1  19405  mplcoe5  19408  mdetunilem9  20366  mdetuni0  20367  maducoeval2  20386  madugsum  20389  isbasis3g  20693  tgcl  20713  tgss2  20731  toponmre  20837  neiptopnei  20876  ist0  21064  ishaus  21066  t0top  21073  haustop  21075  isreg  21076  ist0-2  21088  ist0-3  21089  t1t0  21092  ist1-3  21093  ishaus2  21095  haust1  21096  cmpsublem  21142  cmpsub  21143  tgcmp  21144  hauscmp  21150  bwth  21153  is1stc2  21185  2ndcctbss  21198  2ndcdisj  21199  2ndcdisj2  21200  2ndcomap  21201  2ndcsep  21202  dis2ndc  21203  restnlly  21225  restlly  21226  llyidm  21231  nllyidm  21232  lly1stc  21239  finptfin  21261  locfincmp  21269  ptpjopn  21355  tx1stc  21393  txkgen  21395  xkohaus  21396  xkococnlem  21402  xkoinjcn  21430  ist0-4  21472  kqt0lem  21479  regr1lem2  21483  kqt0  21489  r0sep  21491  nrmr0reg  21492  regr1  21493  kqreg  21494  kqnrm  21495  kqhmph  21562  isfil  21591  filuni  21629  isufil  21647  uffinfix  21671  fmfnfmlem4  21701  hauspwpwf1  21731  alexsublem  21788  alexsubALTlem3  21793  alexsubALTlem4  21794  alexsubALT  21795  ustval  21946  isust  21947  blbas  22175  met1stc  22266  metrest  22269  xrsmopn  22555  cnheibor  22694  jensen  24649  sqff1o  24842  uhgrnbgr0nb  26171  rusgrpropedg  26384  isplig  27216  ispligb  27217  tncp  27218  l2p  27219  eulplig  27225  spanuni  28291  sumdmdii  29162  gsumvsca2  29610  indf1o  29909  gsumesum  29944  dya2iocuni  30168  bnj219  30562  bnj1098  30615  bnj594  30743  bnj580  30744  bnj601  30751  bnj849  30756  bnj996  30786  bnj1006  30790  bnj1029  30797  bnj1033  30798  bnj1090  30808  bnj1110  30811  bnj1124  30817  bnj1128  30819  erdsze  30945  connpconn  30978  rellysconn  30994  cvmsss2  31017  cvmlift2lem12  31057  axextprim  31339  axrepprim  31340  axunprim  31341  axpowprim  31342  axregprim  31343  axinfprim  31344  axacprim  31345  untelirr  31346  untuni  31347  untsucf  31348  unt0  31349  untint  31350  untangtr  31352  dftr6  31401  dffr5  31404  elpotr  31440  dfon2lem3  31444  dfon2lem4  31445  dfon2lem5  31446  dfon2lem6  31447  dfon2lem7  31448  dfon2lem8  31449  dfon2lem9  31450  dfon2  31451  domep  31452  axextdfeq  31457  ax8dfeq  31458  axextdist  31459  axext4dist  31460  exnel  31462  distel  31463  axextndbi  31464  poseq  31504  frrlem11  31546  nobndlem6  31613  nosino  31628  dfiota3  31725  brcup  31741  brcap  31742  dfint3  31754  imagesset  31755  hftr  31984  fness  32039  fneref  32040  neibastop2lem  32050  onsuct0  32135  bj-elequ2g  32361  bj-ax89  32362  bj-elequ12  32363  bj-cleljusti  32364  bj-axext3  32465  bj-axext4  32466  bj-clabel  32479  bj-axrep1  32484  bj-axrep2  32485  bj-axrep3  32486  bj-axrep4  32487  bj-axrep5  32488  bj-axsep  32489  bj-nalset  32490  bj-zfpow  32491  bj-el  32492  bj-dtru  32493  bj-dvdemo1  32498  bj-dvdemo2  32499  bj-nfeel2  32535  bj-axc14nf  32536  bj-axc14  32537  bj-ax8  32587  bj-dfclel  32589  bj-ax9  32590  bj-ax9-2  32591  bj-cleqhyp  32592  bj-dfcleq  32594  bj-axsep2  32621  bj-ru0  32632  bj-ru1  32633  bj-ru  32634  bj-nul  32718  bj-nuliota  32719  bj-nuliotaALT  32720  finixpnum  33065  fin2solem  33066  fin2so  33067  matunitlindflem1  33076  poimirlem30  33110  poimirlem32  33112  poimir  33113  mblfinlem1  33117  mbfresfi  33127  cnambfre  33129  ftc1anc  33164  ftc2nc  33165  cover2g  33180  sstotbnd2  33244  unichnidl  33501  prtlem5  33663  prtlem12  33671  prtlem13  33672  prtlem15  33679  prtlem17  33680  prtlem18  33681  prter1  33683  prter3  33686  ax5el  33741  dveel2ALT  33743  ax12el  33746  pclfinclN  34755  dvh1dim  36250  ismrcd1  36780  dford3lem2  37113  dford4  37115  pw2f1ocnv  37123  pw2f1o2  37124  wepwsolem  37131  fnwe2lem2  37140  aomclem8  37150  kelac1  37152  pwslnm  37183  idomsubgmo  37296  inintabss  37404  inintabd  37405  cnvcnvintabd  37426  intabssd  37436  elintima  37465  dffrege76  37754  frege77  37755  frege89  37767  frege90  37768  frege91  37769  frege93  37771  frege94  37772  frege95  37773  clsk1indlem3  37862  ntrneiel2  37905  ntrneik2  37911  ntrneix2  37912  ntrneik4  37920  gneispa  37949  gneispace2  37951  gneispace3  37952  gneispace  37953  gneispacef  37954  gneispacef2  37955  gneispacern2  37958  gneispace0nelrn  37959  gneispaceel  37962  gneispaceel2  37963  gneispacess  37964  sbcoreleleq  38266  tratrb  38267  ordelordALT  38268  trsbc  38271  truniALT  38272  onfrALTlem5  38278  onfrALTlem4  38279  onfrALTlem3  38280  onfrALTlem2  38282  onfrALTlem1  38284  onfrALT  38285  sspwtrALT  38571  suctrALT2  38594  tratrbVD  38619  truniALTVD  38636  trintALT  38639  onfrALTlem4VD  38644  sprsymrelf1lem  41059  sprsymrelf  41063  dflinc2  41517  lcosslsp  41545  nfintd  41742
  Copyright terms: Public domain W3C validator