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

Theorem wel 2112
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 2112 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 2111. This lets us avoid overloading the connective, thus preventing ambiguity that would complicate certain Metamath parsers. However, logically wel 2112 is considered to be a primitive syntax, even though here it is artificially "derived" from wcel 2111. 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 2111 1 wff 𝑥𝑦
Colors of variables: wff setvar class
Syntax hints:  wcel 2111
This theorem is referenced by:  ax8  2117  elequ1  2118  elsb3  2119  cleljust  2120  ax9  2125  elequ2  2126  elsb4  2127  elequ2g  2128  ax12wdemo  2136  cleljustALT  2371  cleljustALT2  2372  dveel1  2473  dveel2  2474  axc14  2475  axexte  2771  axextg  2772  axextb  2773  axextmo  2774  nulmo  2775  cvjust  2793  ax9ALT  2794  nfcvf  2981  sbabel  2986  rru  3718  ru  3719  eluni  4803  nfunid  4806  unieqOLD  4812  csbuni  4829  inteq  4841  elint  4844  elintg  4846  nfint  4848  int0  4852  intss  4859  uniiun  4945  intiin  4946  axrep1  5155  axreplem  5156  axrep2  5157  axrep3  5158  axrep4  5159  axrep5  5160  axrep6  5161  zfrepclf  5162  axsepgfromrep  5165  axsepg  5168  bm1.3ii  5170  axnul  5173  0ex  5175  nalset  5181  vnex  5182  pwnss  5215  axpweq  5230  zfpow  5232  axpow2  5233  axpow3  5234  el  5235  dtru  5236  dvdemo1  5239  dvdemo2  5240  nfnid  5241  vpwex  5243  axprlem1  5289  axprlem2  5290  axprlem4  5292  axprlem5  5293  axpr  5294  dfepfr  5504  epfrc  5505  wetrep  5512  wefrc  5513  rele  5663  dmep  5757  domepOLD  5758  rnep  5761  ordelord  6181  onfr  6198  funimaexg  6410  zfun  7442  axun2  7443  uniex2  7444  uniuni  7464  epweon  7477  onint  7490  ordom  7569  wfrlem12  7949  dfsmo2  7967  issmo  7968  smores2  7974  smo11  7984  smogt  7987  dfrecs3  7992  tz7.48lem  8060  tz7.48-2  8061  omeulem1  8191  pw2eng  8606  infensuc  8679  1sdom  8705  unxpdomlem1  8706  unxpdomlem2  8707  unxpdomlem3  8708  pssnn  8720  findcard2  8742  findcard2d  8744  ac6sfi  8746  frfi  8747  fissuni  8813  axreg2  9041  zfregcl  9042  epinid0  9048  cnvepnep  9055  dford2  9067  inf0  9068  inf1  9069  inf2  9070  zfinf  9086  axinf2  9087  zfinf2  9089  axinf  9091  dfom4  9096  dfom5  9097  unbnn3  9106  noinfep  9107  cantnf  9140  epfrs  9157  r111  9188  dif1card  9421  alephle  9499  aceq1  9528  aceq0  9529  aceq2  9530  dfac3  9532  dfac5lem2  9535  dfac5lem4  9537  dfac5  9539  dfac2a  9540  dfac2b  9541  dfac2  9542  dfac7  9543  dfac0  9544  dfac1  9545  kmlem2  9562  kmlem3  9563  kmlem4  9564  kmlem5  9565  kmlem8  9568  kmlem14  9574  kmlem15  9575  dfackm  9577  ackbij1lem10  9640  coflim  9672  cflim2  9674  cfsmolem  9681  fin23lem26  9736  ituniiun  9833  domtriomlem  9853  axdc3lem2  9862  zfac  9871  ac2  9872  ac3  9873  axac3  9875  axac2  9877  axac  9878  nd1  9998  nd2  9999  nd3  10000  nd4  10001  axextnd  10002  axrepndlem1  10003  axrepndlem2  10004  axrepnd  10005  axunndlem1  10006  axunnd  10007  axpowndlem1  10008  axpowndlem2  10009  axpowndlem3  10010  axpowndlem4  10011  axpownd  10012  axregndlem1  10013  axregndlem2  10014  axregnd  10015  axinfndlem1  10016  axinfnd  10017  axacndlem1  10018  axacndlem2  10019  axacndlem3  10020  axacndlem4  10021  axacndlem5  10022  axacnd  10023  fpwwe2lem12  10052  inar1  10186  axgroth5  10235  axgroth2  10236  grothpw  10237  axgroth6  10239  grothomex  10240  axgroth3  10242  axgroth4  10243  grothprimlem  10244  grothprim  10245  inaprc  10247  nqereu  10340  npex  10397  elnpi  10399  hashbclem  13806  fsum2dlem  15117  fprod2dlem  15326  fprod2d  15327  rpnnen2  15571  lcmfunsnlem2lem2  15973  ismre  16853  fnmre  16854  mremre  16867  isacs  16914  isacs1i  16920  mreacs  16921  acsfn1  16924  acsfn2  16926  isacs3lem  17768  pmtrprfval  18607  pmtrsn  18639  gsum2dlem2  19084  lbsextlem4  19926  drngnidl  19995  mplcoe1  20705  mplcoe5  20708  selvffval  20788  selvfval  20789  mdetunilem9  21225  mdetuni0  21226  maducoeval2  21245  madugsum  21248  isbasis3g  21554  tgcl  21574  tgss2  21592  toponmre  21698  neiptopnei  21737  ist0  21925  ishaus  21927  t0top  21934  haustop  21936  isreg  21937  ist0-2  21949  ist0-3  21950  t1t0  21953  ist1-3  21954  ishaus2  21956  haust1  21957  cmpsublem  22004  cmpsub  22005  tgcmp  22006  hauscmp  22012  bwth  22015  is1stc2  22047  2ndcctbss  22060  2ndcdisj  22061  2ndcdisj2  22062  2ndcomap  22063  2ndcsep  22064  dis2ndc  22065  restnlly  22087  restlly  22088  llyidm  22093  nllyidm  22094  lly1stc  22101  finptfin  22123  locfincmp  22131  comppfsc  22137  ptpjopn  22217  tx1stc  22255  txkgen  22257  xkohaus  22258  xkococnlem  22264  xkoinjcn  22292  ist0-4  22334  kqt0lem  22341  regr1lem2  22345  kqt0  22351  r0sep  22353  nrmr0reg  22354  regr1  22355  kqreg  22356  kqnrm  22357  kqhmph  22424  isfil  22452  filuni  22490  isufil  22508  uffinfix  22532  fmfnfmlem4  22562  hauspwpwf1  22592  alexsublem  22649  alexsubALTlem3  22654  alexsubALTlem4  22655  alexsubALT  22656  ustval  22808  isust  22809  blbas  23037  met1stc  23128  metrest  23131  xrsmopn  23417  cnheibor  23560  itg2cn  24367  jensen  25574  sqff1o  25767  f1otrg  26665  uhgrnbgr0nb  27144  rusgrpropedg  27374  isplig  28259  ispligb  28260  tncp  28261  l2p  28262  eulplig  28268  spanuni  29327  sumdmdii  30198  gsumvsca2  30905  fedgmul  31115  extdg1id  31141  indf1o  31393  gsumesum  31428  dya2iocuni  31651  bnj219  32113  bnj1098  32165  bnj594  32294  bnj580  32295  bnj601  32302  bnj849  32307  bnj996  32338  bnj1006  32342  bnj1029  32350  bnj1033  32351  bnj1090  32361  bnj1110  32364  bnj1124  32370  bnj1128  32372  erdsze  32562  connpconn  32595  rellysconn  32611  cvmsss2  32634  cvmlift2lem12  32674  axextprim  33040  axrepprim  33041  axunprim  33042  axpowprim  33043  axregprim  33044  axinfprim  33045  axacprim  33046  untelirr  33047  untuni  33048  untsucf  33049  unt0  33050  untint  33051  untangtr  33053  dftr6  33099  dffr5  33102  elpotr  33139  dfon2lem3  33143  dfon2lem4  33144  dfon2lem5  33145  dfon2lem6  33146  dfon2lem7  33147  dfon2lem8  33148  dfon2lem9  33149  dfon2  33150  axextdfeq  33155  ax8dfeq  33156  axextdist  33157  axextbdist  33158  exnel  33160  distel  33161  axextndbi  33162  poseq  33208  frrlem4  33239  frrlem8  33243  frrlem10  33245  nosupno  33316  dfiota3  33497  brcup  33513  brcap  33514  dfint3  33526  imagesset  33527  hftr  33756  fness  33810  fneref  33811  neibastop2lem  33821  onsuct0  33902  bj-ax89  34124  bj-elequ12  34125  bj-cleljusti  34126  bj-dtru  34254  bj-nfeel2  34293  bj-axc14nf  34294  bj-axc14  34295  eliminable-veqab  34304  eliminable-abeqv  34305  eliminable-abelv  34307  eliminable-abelab  34308  bj-ax9  34340  bj-zfauscl  34367  bj-ru0  34377  bj-ru1  34378  bj-ru  34379  currysetlem  34380  curryset  34381  currysetlem1  34382  currysetlem3  34384  currysetALT  34385  bj-nul  34473  bj-nuliota  34474  bj-nuliotaALT  34475  bj-bm1.3ii  34481  bj-epelg  34484  finixpnum  35042  fin2solem  35043  fin2so  35044  matunitlindflem1  35053  poimirlem30  35087  poimirlem32  35089  poimir  35090  mblfinlem1  35094  mbfresfi  35103  cnambfre  35105  ftc1anc  35138  ftc2nc  35139  cover2g  35153  sstotbnd2  35212  unichnidl  35469  dfcoels  35835  dfeldisj5  36114  prtlem5  36156  prtlem12  36163  prtlem13  36164  prtlem16  36165  prtlem15  36171  prtlem17  36172  prtlem18  36173  prter1  36175  prter3  36178  ax5el  36233  dveel2ALT  36235  ax12el  36238  pclfinclN  37246  dvh1dim  38738  sn-axrep5v  39398  sn-axprlem3  39399  sn-el  39400  sn-dtru  39401  prjspval  39595  ismrcd1  39637  dford3lem2  39966  dford4  39968  pw2f1ocnv  39976  pw2f1o2  39977  wepwsolem  39984  fnwe2lem2  39993  aomclem8  40003  kelac1  40005  pwslnm  40036  idomsubgmo  40140  intabssd  40225  eu0  40226  ontric3g  40228  alephiso2  40255  inintabss  40276  inintabd  40277  cnvcnvintabd  40298  elintima  40352  dffrege76  40638  frege77  40639  frege89  40651  frege90  40652  frege91  40653  frege93  40655  frege94  40656  frege95  40657  clsk1indlem3  40744  ntrneiel2  40787  ntrneik2  40793  ntrneix2  40794  ntrneik4  40802  gneispa  40831  gneispace2  40833  gneispace3  40834  gneispace  40835  gneispacef  40836  gneispacef2  40837  gneispacern2  40840  gneispace0nelrn  40841  gneispaceel  40844  gneispaceel2  40845  gneispacess  40846  ismnu  40967  mnuop123d  40968  mnussd  40969  mnuop23d  40972  mnupwd  40973  mnuop3d  40977  mnuprdlem4  40981  mnutrd  40986  grumnudlem  40991  ismnuprim  41000  rr-grothprimbi  41001  rr-grothprim  41006  sbcoreleleq  41239  tratrb  41240  ordelordALT  41241  trsbc  41244  truniALT  41245  onfrALTlem5  41246  onfrALTlem4  41247  onfrALTlem3  41248  onfrALTlem2  41250  onfrALTlem1  41252  onfrALT  41253  sspwtrALT  41526  suctrALT2  41541  tratrbVD  41565  truniALTVD  41582  trintALT  41585  onfrALTlem4VD  41590  iota0ndef  43629  aiota0ndef  43650  ralndv1  43659  dfnelbr2  43827  nelbr  43828  nelbrim  43829  sprsymrelf1lem  44006  sprsymrelf  44010  paireqne  44026  dflinc2  44817  lcosslsp  44845  nfintd  45201
  Copyright terms: Public domain W3C validator