Theorem wel 1991

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 1991 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 1990. This lets us avoid overloading the ∈ connective, thus preventing ambiguity that would complicate certain Metamath parsers. However, logically wel 1991 is considered to be a primitive syntax, even though here it is artificially "derived" from wcel 1990. 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

Step	Hyp	Ref	Expression
1		wcel 1990	1 wff 𝑥 ∈ 𝑦

Syntax hints:   ∈ wcel 1990

This theorem is referenced by:  ax8  1996  elequ1  1997  cleljust  1998  ax9  2003  elequ2  2004  ax12wdemo  2012  cleljustALT  2185  cleljustALT2  2186  dveel1  2370  dveel2  2371  axc14  2372  elsb3  2434  elsb4  2435  axext2  2603  axext3  2604  axext3ALT  2605  axext4  2606  bm1.1  2607  sbabel  2793  ru  3434  nfuni  4442  nfunid  4443  unieq  4444  csbuni  4466  inteq  4478  elintg  4483  nfint  4486  int0  4490  intss  4498  uniiun  4573  intiin  4574  trint  4768  trintssOLD  4770  axrep1  4772  axrep2  4773  axrep3  4774  axrep4  4775  axrep5  4776  zfrepclf  4777  axsep  4780  axsep2  4782  bm1.3ii  4784  zfnuleu  4786  axnul  4788  0ex  4790  nalset  4795  axpweq  4842  zfpow  4844  axpow2  4845  axpow3  4846  el  4847  dtru  4857  nfnid  4897  dvdemo1  4902  dvdemo2  4903  dfepfr  5099  wetrep  5107  wefrc  5108  rele  5250  ordelord  5745  onfr  5763  funimaexg  5975  zfun  6950  axun2  6951  uniuni  6971  onint  6995  ordom  7074  wfrlem12  7426  dfsmo2  7444  smores2  7451  smo11  7461  smogt  7464  dfrecs3  7469  tz7.48lem  7536  tz7.48-2  7537  omeulem1  7662  pw2eng  8066  infensuc  8138  1sdom  8163  unxpdomlem1  8164  unxpdomlem2  8165  unxpdomlem3  8166  pssnn  8178  findcard2  8200  findcard2d  8202  ac6sfi  8204  frfi  8205  fissuni  8271  axreg2  8498  zfregcl  8499  zfregclOLD  8501  dford2  8517  inf0  8518  inf1  8519  inf2  8520  zfinf  8536  axinf2  8537  zfinf2  8539  dfom4  8546  dfom5  8547  unbnn3  8556  noinfep  8557  cantnf  8590  epfrs  8607  r111  8638  dif1card  8833  alephle  8911  aceq1  8940  aceq0  8941  aceq2  8942  dfac3  8944  dfac5lem2  8947  dfac5lem4  8949  dfac5  8951  dfac2a  8952  dfac2  8953  dfac7  8954  dfac0  8955  dfac1  8956  kmlem3  8974  kmlem4  8975  kmlem5  8976  kmlem8  8979  kmlem14  8985  kmlem15  8986  dfackm  8988  ackbij1lem10  9051  coflim  9083  cflim2  9085  cfsmolem  9092  fin23lem26  9147  ituniiun  9244  domtriomlem  9264  axdc3lem2  9273  zfac  9282  ac2  9283  ac3  9284  axac3  9286  axac2  9288  axac  9289  nd1  9409  nd2  9410  nd3  9411  nd4  9412  axextnd  9413  axrepndlem1  9414  axrepndlem2  9415  axrepnd  9416  axunndlem1  9417  axunnd  9418  axpowndlem1  9419  axpowndlem2  9420  axpowndlem3  9421  axpowndlem4  9422  axpownd  9423  axregndlem1  9424  axregndlem2  9425  axregnd  9426  axinfndlem1  9427  axinfnd  9428  axacndlem1  9429  axacndlem2  9430  axacndlem3  9431  axacndlem4  9432  axacndlem5  9433  axacnd  9434  fpwwe2lem12  9463  inar1  9597  axgroth5  9646  axgroth2  9647  grothpw  9648  axgroth6  9650  grothomex  9651  axgroth3  9653  axgroth4  9654  grothprimlem  9655  grothprim  9656  nqereu  9751  npex  9808  elnpi  9810  hashbclem  13236  brfi1uzindOLD  13286  brfi1indALTOLD  13288  opfi1uzindOLD  13289  fsum2dlem  14501  fprod2dlem  14710  fprod2d  14711  rpnnen2  14955  lcmfunsnlem2lem2  15352  ismre  16250  fnmre  16251  mremre  16264  isacs  16312  isacs1i  16318  mreacs  16319  acsfn1  16322  acsfn2  16324  isacs3lem  17166  pmtrprfval  17907  pmtrsn  17939  gsum2dlem2  18370  lbsextlem4  19161  drngnidl  19229  mplcoe1  19465  mplcoe5  19468  mdetunilem9  20426  mdetuni0  20427  maducoeval2  20446  madugsum  20449  isbasis3g  20753  tgcl  20773  tgss2  20791  toponmre  20897  neiptopnei  20936  ist0  21124  ishaus  21126  t0top  21133  haustop  21135  isreg  21136  ist0-2  21148  ist0-3  21149  t1t0  21152  ist1-3  21153  ishaus2  21155  haust1  21156  cmpsublem  21202  cmpsub  21203  tgcmp  21204  hauscmp  21210  bwth  21213  is1stc2  21245  2ndcctbss  21258  2ndcdisj  21259  2ndcdisj2  21260  2ndcomap  21261  2ndcsep  21262  dis2ndc  21263  restnlly  21285  restlly  21286  llyidm  21291  nllyidm  21292  lly1stc  21299  finptfin  21321  locfincmp  21329  ptpjopn  21415  tx1stc  21453  txkgen  21455  xkohaus  21456  xkococnlem  21462  xkoinjcn  21490  ist0-4  21532  kqt0lem  21539  regr1lem2  21543  kqt0  21549  r0sep  21551  nrmr0reg  21552  regr1  21553  kqreg  21554  kqnrm  21555  kqhmph  21622  isfil  21651  filuni  21689  isufil  21707  uffinfix  21731  fmfnfmlem4  21761  hauspwpwf1  21791  alexsublem  21848  alexsubALTlem3  21853  alexsubALTlem4  21854  alexsubALT  21855  ustval  22006  isust  22007  blbas  22235  met1stc  22326  metrest  22329  xrsmopn  22615  cnheibor  22754  jensen  24715  sqff1o  24908  uhgrnbgr0nb  26250  rusgrpropedg  26480  isplig  27328  ispligb  27329  tncp  27330  l2p  27331  eulplig  27337  spanuni  28403  sumdmdii  29274  gsumvsca2  29783  indf1o  30086  gsumesum  30121  dya2iocuni  30345  bnj219  30801  bnj1098  30854  bnj594  30982  bnj580  30983  bnj601  30990  bnj849  30995  bnj996  31025  bnj1006  31029  bnj1029  31036  bnj1033  31037  bnj1090  31047  bnj1110  31050  bnj1124  31056  bnj1128  31058  erdsze  31184  connpconn  31217  rellysconn  31233  cvmsss2  31256  cvmlift2lem12  31296  axextprim  31578  axrepprim  31579  axunprim  31580  axpowprim  31581  axregprim  31582  axinfprim  31583  axacprim  31584  untelirr  31585  untuni  31586  untsucf  31587  unt0  31588  untint  31589  untangtr  31591  dftr6  31640  dffr5  31643  elpotr  31686  dfon2lem3  31690  dfon2lem4  31691  dfon2lem5  31692  dfon2lem6  31693  dfon2lem7  31694  dfon2lem8  31695  dfon2lem9  31696  dfon2  31697  domep  31698  axextdfeq  31703  ax8dfeq  31704  axextdist  31705  axext4dist  31706  exnel  31708  distel  31709  axextndbi  31710  poseq  31750  frrlem11  31792  nosupno  31849  dfiota3  32030  brcup  32046  brcap  32047  dfint3  32059  imagesset  32060  hftr  32289  fness  32344  fneref  32345  neibastop2lem  32355  onsuct0  32440  bj-elequ2g  32666  bj-ax89  32667  bj-elequ12  32668  bj-cleljusti  32669  bj-axext3  32769  bj-axext4  32770  bj-clabel  32783  bj-axrep1  32788  bj-axrep2  32789  bj-axrep3  32790  bj-axrep4  32791  bj-axrep5  32792  bj-axsep  32793  bj-nalset  32794  bj-zfpow  32795  bj-el  32796  bj-dtru  32797  bj-dvdemo1  32802  bj-dvdemo2  32803  bj-nfeel2  32837  bj-axc14nf  32838  bj-axc14  32839  bj-ax8  32887  bj-dfclel  32889  bj-ax9  32890  bj-ax9-2  32891  bj-cleqhyp  32892  bj-dfcleq  32894  bj-axsep2  32921  bj-ru0  32932  bj-ru1  32933  bj-ru  32934  bj-nul  33018  bj-nuliota  33019  bj-nuliotaALT  33020  finixpnum  33394  fin2solem  33395  fin2so  33396  matunitlindflem1  33405  poimirlem30  33439  poimirlem32  33441  poimir  33442  mblfinlem1  33446  mbfresfi  33456  cnambfre  33458  ftc1anc  33493  ftc2nc  33494  cover2g  33509  sstotbnd2  33573  unichnidl  33830  prtlem5  34145  prtlem12  34152  prtlem13  34153  prtlem15  34160  prtlem17  34161  prtlem18  34162  prter1  34164  prter3  34167  ax5el  34222  dveel2ALT  34224  ax12el  34227  pclfinclN  35236  dvh1dim  36731  ismrcd1  37261  dford3lem2  37594  dford4  37596  pw2f1ocnv  37604  pw2f1o2  37605  wepwsolem  37612  fnwe2lem2  37621  aomclem8  37631  kelac1  37633  pwslnm  37664  idomsubgmo  37776  inintabss  37884  inintabd  37885  cnvcnvintabd  37906  intabssd  37916  elintima  37945  dffrege76  38233  frege77  38234  frege89  38246  frege90  38247  frege91  38248  frege93  38250  frege94  38251  frege95  38252  clsk1indlem3  38341  ntrneiel2  38384  ntrneik2  38390  ntrneix2  38391  ntrneik4  38399  gneispa  38428  gneispace2  38430  gneispace3  38431  gneispace  38432  gneispacef  38433  gneispacef2  38434  gneispacern2  38437  gneispace0nelrn  38438  gneispaceel  38441  gneispaceel2  38442  gneispacess  38443  sbcoreleleq  38745  tratrb  38746  ordelordALT  38747  trsbc  38750  truniALT  38751  onfrALTlem5  38757  onfrALTlem4  38758  onfrALTlem3  38759  onfrALTlem2  38761  onfrALTlem1  38763  onfrALT  38764  sspwtrALT  39049  suctrALT2  39072  tratrbVD  39097  truniALTVD  39114  trintALT  39117  onfrALTlem4VD  39122  dfnelbr2  41290  nelbr  41291  nelbrim  41292  sprsymrelf1lem  41741  sprsymrelf  41745  dflinc2  42199  lcosslsp  42227  nfintd  42420