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

Theorem wel 2158
Description: Extend wff definition to include atomic formulas with the 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 (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 2158 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 2157. This lets us avoid overloading the connective, thus preventing ambiguity that would complicate certain Metamath parsers. However, logically wel 2158 is considered to be a primitive syntax, even though here it is artificially "derived" from wcel 2157. 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 2157 1 wff 𝑥𝑦
Colors of variables: wff setvar class
Syntax hints:  wcel 2157
This theorem is referenced by:  ax8  2163  elequ1  2164  cleljust  2165  ax9  2170  elequ2  2171  ax12wdemo  2179  cleljustALT  2361  cleljustALT2  2362  dveel1  2531  dveel2  2532  axc14  2533  elsb3lem  2597  elsb3  2598  elsb3OLD  2599  elsb4lem  2600  elsb4  2601  elsb4OLD  2602  axext2  2796  axext3  2797  axext3ALT  2798  axext4  2799  axextmo  2800  bm1.1OLD  2801  nulmo  2802  sbabel  2988  ru  3643  nfuni  4647  nfunid  4648  unieq  4649  csbuni  4671  inteq  4683  elintg  4688  nfint  4690  int0  4694  intss  4701  uniiun  4776  intiin  4777  trintOLD  4974  trintssOLD  4976  axrep1  4978  axreplem  4979  axrep2  4980  axrep3  4981  axrep4  4982  axrep5  4983  zfrepclf  4984  axsep  4987  axsep2  4989  bm1.3ii  4991  zfnuleuOLD  4993  axnul  4995  0ex  4997  nalset  5003  vnex  5004  axpweq  5047  zfpow  5049  axpow2  5050  axpow3  5051  el  5052  dtru  5053  dvdemo1  5056  dvdemo2  5057  nfnid  5058  vpwex  5060  dfepfr  5309  wetrep  5317  wefrc  5318  rele  5466  ordelord  5972  onfr  5989  funimaexg  6196  zfun  7190  axun2  7191  uniuni  7211  onint  7235  ordom  7314  wfrlem12  7672  dfsmo2  7690  smores2  7697  smo11  7707  smogt  7710  dfrecs3  7715  tz7.48lem  7782  tz7.48-2  7783  omeulem1  7909  pw2eng  8315  infensuc  8387  1sdom  8412  unxpdomlem1  8413  unxpdomlem2  8414  unxpdomlem3  8415  pssnn  8427  findcard2  8449  findcard2d  8451  ac6sfi  8453  frfi  8454  fissuni  8520  axreg2  8747  zfregcl  8748  epinid0  8754  cnvepnep  8760  dford2  8774  inf0  8775  inf1  8776  inf2  8777  zfinf  8793  axinf2  8794  zfinf2  8796  dfom4  8803  dfom5  8804  unbnn3  8813  noinfep  8814  cantnf  8847  epfrs  8864  r111  8895  dif1card  9126  alephle  9204  aceq1  9233  aceq0  9234  aceq2  9235  dfac3  9237  dfac5lem2  9240  dfac5lem4  9242  dfac5  9244  dfac2a  9245  dfac2  9247  dfac2OLD  9248  dfac7  9249  dfac0  9250  dfac1  9251  kmlem3  9269  kmlem4  9270  kmlem5  9271  kmlem8  9274  kmlem14  9280  kmlem15  9281  dfackm  9283  ackbij1lem10  9346  coflim  9378  cflim2  9380  cfsmolem  9387  fin23lem26  9442  ituniiun  9539  domtriomlem  9559  axdc3lem2  9568  zfac  9577  ac2  9578  ac3  9579  axac3  9581  axac2  9583  axac  9584  nd1  9704  nd2  9705  nd3  9706  nd4  9707  axextnd  9708  axrepndlem1  9709  axrepndlem2  9710  axrepnd  9711  axunndlem1  9712  axunnd  9713  axpowndlem1  9714  axpowndlem2  9715  axpowndlem3  9716  axpowndlem4  9717  axpownd  9718  axregndlem1  9719  axregndlem2  9720  axregnd  9721  axinfndlem1  9722  axinfnd  9723  axacndlem1  9724  axacndlem2  9725  axacndlem3  9726  axacndlem4  9727  axacndlem5  9728  axacnd  9729  inar1  9892  axgroth5  9941  axgroth2  9942  grothpw  9943  axgroth6  9945  grothomex  9946  axgroth3  9948  axgroth4  9949  grothprimlem  9950  grothprim  9951  nqereu  10046  npex  10103  elnpi  10105  hashbclem  13473  fsum2dlem  14744  fprod2dlem  14951  fprod2d  14952  rpnnen2  15195  lcmfunsnlem2lem2  15591  ismre  16475  fnmre  16476  mremre  16489  isacs  16536  isacs1i  16542  mreacs  16543  acsfn1  16546  acsfn2  16548  isacs3lem  17391  pmtrprfval  18128  pmtrsn  18160  gsum2dlem2  18591  lbsextlem4  19390  drngnidl  19458  mplcoe1  19694  mplcoe5  19697  mdetunilem9  20658  mdetuni0  20659  maducoeval2  20678  madugsum  20681  isbasis3g  20988  tgcl  21008  tgss2  21026  toponmre  21132  neiptopnei  21171  ist0  21359  ishaus  21361  t0top  21368  haustop  21370  isreg  21371  ist0-2  21383  ist0-3  21384  t1t0  21387  ist1-3  21388  ishaus2  21390  haust1  21391  cmpsublem  21437  cmpsub  21438  tgcmp  21439  hauscmp  21445  bwth  21448  is1stc2  21480  2ndcctbss  21493  2ndcdisj  21494  2ndcdisj2  21495  2ndcomap  21496  2ndcsep  21497  dis2ndc  21498  restnlly  21520  restlly  21521  llyidm  21526  nllyidm  21527  lly1stc  21534  finptfin  21556  locfincmp  21564  ptpjopn  21650  tx1stc  21688  txkgen  21690  xkohaus  21691  xkococnlem  21697  xkoinjcn  21725  ist0-4  21767  kqt0lem  21774  regr1lem2  21778  kqt0  21784  r0sep  21786  nrmr0reg  21787  regr1  21788  kqreg  21789  kqnrm  21790  kqhmph  21857  isfil  21885  filuni  21923  isufil  21941  uffinfix  21965  fmfnfmlem4  21995  hauspwpwf1  22025  alexsublem  22082  alexsubALTlem3  22087  alexsubALTlem4  22088  alexsubALT  22089  ustval  22240  isust  22241  blbas  22469  met1stc  22560  metrest  22563  xrsmopn  22849  cnheibor  22988  jensen  24952  sqff1o  25145  uhgrnbgr0nb  26489  rusgrpropedg  26731  isplig  27682  ispligb  27683  tncp  27684  l2p  27685  eulplig  27691  spanuni  28754  sumdmdii  29625  gsumvsca2  30131  indf1o  30434  gsumesum  30469  dya2iocuni  30693  bnj219  31147  bnj1098  31199  bnj594  31327  bnj580  31328  bnj601  31335  bnj849  31340  bnj996  31370  bnj1006  31374  bnj1029  31381  bnj1033  31382  bnj1090  31392  bnj1110  31395  bnj1124  31401  bnj1128  31403  erdsze  31529  connpconn  31562  rellysconn  31578  cvmsss2  31601  cvmlift2lem12  31641  axextprim  31922  axrepprim  31923  axunprim  31924  axpowprim  31925  axregprim  31926  axinfprim  31927  axacprim  31928  untelirr  31929  untuni  31930  untsucf  31931  unt0  31932  untint  31933  untangtr  31935  dftr6  31984  dffr5  31987  elpotr  32028  dfon2lem3  32032  dfon2lem4  32033  dfon2lem5  32034  dfon2lem6  32035  dfon2lem7  32036  dfon2lem8  32037  dfon2lem9  32038  dfon2  32039  domep  32040  axextdfeq  32045  ax8dfeq  32046  axextdist  32047  axext4dist  32048  exnel  32050  distel  32051  axextndbi  32052  poseq  32096  frrlem4  32126  frrlem11  32135  nosupno  32192  dfiota3  32373  brcup  32389  brcap  32390  dfint3  32402  imagesset  32403  hftr  32632  fness  32687  fneref  32688  neibastop2lem  32698  onsuct0  32779  bj-elequ2g  33003  bj-ax89  33004  bj-elequ12  33005  bj-cleljusti  33006  bj-axext3  33102  bj-axext4  33103  bj-clabel  33116  bj-axrep1  33121  bj-axrep2  33122  bj-axrep3  33123  bj-axrep4  33124  bj-axrep5  33125  bj-axsep  33126  bj-nalset  33127  bj-zfpow  33128  bj-el  33129  bj-dtru  33130  bj-dvdemo1  33135  bj-dvdemo2  33136  bj-nfeel2  33168  bj-axc14nf  33169  bj-axc14  33170  bj-ax8  33214  bj-dfclel  33216  bj-ax9  33217  bj-ax9-2  33218  bj-cleqhyp  33219  bj-dfcleq  33221  bj-axsep2  33250  bj-zfauscl  33251  bj-ru0  33262  bj-ru1  33263  bj-ru  33264  bj-nul  33347  bj-nuliota  33348  bj-nuliotaALT  33349  bj-bm1.3ii  33353  finixpnum  33726  fin2solem  33727  fin2so  33728  matunitlindflem1  33737  poimirlem30  33771  poimirlem32  33773  poimir  33774  mblfinlem1  33778  mbfresfi  33787  cnambfre  33789  ftc1anc  33824  ftc2nc  33825  cover2g  33840  sstotbnd2  33903  unichnidl  34160  prtlem5  34658  prtlem12  34665  prtlem13  34666  prtlem15  34673  prtlem17  34674  prtlem18  34675  prter1  34677  prter3  34680  ax5el  34735  dveel2ALT  34737  ax12el  34740  pclfinclN  35749  dvh1dim  37241  ismrcd1  37781  dford3lem2  38113  dford4  38115  pw2f1ocnv  38123  pw2f1o2  38124  wepwsolem  38131  fnwe2lem2  38140  aomclem8  38150  kelac1  38152  pwslnm  38183  idomsubgmo  38295  inintabss  38402  inintabd  38403  cnvcnvintabd  38424  intabssd  38434  elintima  38463  dffrege76  38751  frege77  38752  frege89  38764  frege90  38765  frege91  38766  frege93  38768  frege94  38769  frege95  38770  clsk1indlem3  38859  ntrneiel2  38902  ntrneik2  38908  ntrneix2  38909  ntrneik4  38917  gneispa  38946  gneispace2  38948  gneispace3  38949  gneispace  38950  gneispacef  38951  gneispacef2  38952  gneispacern2  38955  gneispace0nelrn  38956  gneispaceel  38959  gneispaceel2  38960  gneispacess  38961  sbcoreleleq  39261  tratrb  39262  ordelordALT  39263  trsbc  39266  truniALT  39267  onfrALTlem5  39273  onfrALTlem4  39274  onfrALTlem3  39275  onfrALTlem2  39277  onfrALTlem1  39279  onfrALT  39280  sspwtrALT  39564  suctrALT2  39584  tratrbVD  39609  truniALTVD  39626  trintALT  39629  onfrALTlem4VD  39634  iota0ndef  41676  aiota0ndef  41697  dfnelbr2  41880  nelbr  41881  nelbrim  41882  sprsymrelf1lem  42327  sprsymrelf  42331  dflinc2  42785  lcosslsp  42813  nfintd  43006
  Copyright terms: Public domain W3C validator