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

Theorem wel 2082
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 2082 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 2081. This lets us avoid overloading the connective, thus preventing ambiguity that would complicate certain Metamath parsers. However, logically wel 2082 is considered to be a primitive syntax, even though here it is artificially "derived" from wcel 2081. 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 2081 1 wff 𝑥𝑦
Colors of variables: wff setvar class
Syntax hints:  wcel 2081
This theorem is referenced by:  ax8  2087  elequ1  2088  elsb3  2089  cleljust  2090  ax9  2095  elequ2  2096  elsb4  2097  elequ2g  2098  ax12wdemo  2106  cleljustALT  2339  cleljustALT2  2340  dveel1  2441  dveel2  2442  axc14  2443  axexte  2770  axextg  2771  axextb  2772  axextmo  2773  nulmo  2774  cvjust  2790  ax9ALT  2791  nfcvf  2975  sbabel  2983  rru  3704  ru  3705  nfuni  4751  nfunid  4752  unieq  4753  csbuni  4773  inteq  4785  elintg  4790  nfint  4792  int0  4796  intss  4803  uniiun  4881  intiin  4882  axrep1  5082  axreplem  5083  axrep2  5084  axrep3  5085  axrep4  5086  axrep5  5087  axrep6  5088  zfrepclf  5089  axsepgfromrep  5092  axsepg  5095  bm1.3ii  5097  axnul  5100  0ex  5102  nalset  5108  vnex  5109  pwnss  5141  axpweq  5156  zfpow  5158  axpow2  5159  axpow3  5160  el  5161  dtru  5162  dvdemo1  5165  dvdemo2  5166  nfnid  5167  vpwex  5169  axprlem1  5215  axprlem2  5216  axprlem4  5218  axprlem5  5219  axpr  5220  dfepfr  5428  epfrc  5429  wetrep  5436  wefrc  5437  rele  5585  ordelord  6088  onfr  6105  funimaexg  6310  zfun  7320  axun2  7321  uniuni  7341  epweon  7353  onint  7366  ordom  7445  wfrlem12  7818  dfsmo2  7836  issmo  7837  smores2  7843  smo11  7853  smogt  7856  dfrecs3  7861  tz7.48lem  7928  tz7.48-2  7929  omeulem1  8058  pw2eng  8470  infensuc  8542  1sdom  8567  unxpdomlem1  8568  unxpdomlem2  8569  unxpdomlem3  8570  pssnn  8582  findcard2  8604  findcard2d  8606  ac6sfi  8608  frfi  8609  fissuni  8675  axreg2  8903  zfregcl  8904  epinid0  8910  cnvepnep  8917  dford2  8929  inf0  8930  inf1  8931  inf2  8932  zfinf  8948  axinf2  8949  zfinf2  8951  dfom4  8958  dfom5  8959  unbnn3  8968  noinfep  8969  cantnf  9002  epfrs  9019  r111  9050  dif1card  9282  alephle  9360  aceq1  9389  aceq0  9390  aceq2  9391  dfac3  9393  dfac5lem2  9396  dfac5lem4  9398  dfac5  9400  dfac2a  9401  dfac2b  9402  dfac2  9403  dfac7  9404  dfac0  9405  dfac1  9406  kmlem2  9423  kmlem3  9424  kmlem4  9425  kmlem5  9426  kmlem8  9429  kmlem14  9435  kmlem15  9436  dfackm  9438  ackbij1lem10  9497  coflim  9529  cflim2  9531  cfsmolem  9538  fin23lem26  9593  ituniiun  9690  domtriomlem  9710  axdc3lem2  9719  zfac  9728  ac2  9729  ac3  9730  axac3  9732  axac2  9734  axac  9735  nd1  9855  nd2  9856  nd3  9857  nd4  9858  axextnd  9859  axrepndlem1  9860  axrepndlem2  9861  axrepnd  9862  axunndlem1  9863  axunnd  9864  axpowndlem1  9865  axpowndlem2  9866  axpowndlem3  9867  axpowndlem4  9868  axpownd  9869  axregndlem1  9870  axregndlem2  9871  axregnd  9872  axinfndlem1  9873  axinfnd  9874  axacndlem1  9875  axacndlem2  9876  axacndlem3  9877  axacndlem4  9878  axacndlem5  9879  axacnd  9880  fpwwe2lem12  9909  inar1  10043  axgroth5  10092  axgroth2  10093  grothpw  10094  axgroth6  10096  grothomex  10097  axgroth3  10099  axgroth4  10100  grothprimlem  10101  grothprim  10102  inaprc  10104  nqereu  10197  npex  10254  elnpi  10256  hashbclem  13658  fsum2dlem  14958  fprod2dlem  15167  fprod2d  15168  rpnnen2  15412  lcmfunsnlem2lem2  15812  ismre  16690  fnmre  16691  mremre  16704  isacs  16751  isacs1i  16757  mreacs  16758  acsfn1  16761  acsfn2  16763  isacs3lem  17605  pmtrprfval  18346  pmtrsn  18378  gsum2dlem2  18811  lbsextlem4  19623  drngnidl  19691  mplcoe1  19933  mplcoe5  19936  selvffval  20012  selvfval  20013  mdetunilem9  20913  mdetuni0  20914  maducoeval2  20933  madugsum  20936  isbasis3g  21241  tgcl  21261  tgss2  21279  toponmre  21385  neiptopnei  21424  ist0  21612  ishaus  21614  t0top  21621  haustop  21623  isreg  21624  ist0-2  21636  ist0-3  21637  t1t0  21640  ist1-3  21641  ishaus2  21643  haust1  21644  cmpsublem  21691  cmpsub  21692  tgcmp  21693  hauscmp  21699  bwth  21702  is1stc2  21734  2ndcctbss  21747  2ndcdisj  21748  2ndcdisj2  21749  2ndcomap  21750  2ndcsep  21751  dis2ndc  21752  restnlly  21774  restlly  21775  llyidm  21780  nllyidm  21781  lly1stc  21788  finptfin  21810  locfincmp  21818  comppfsc  21824  ptpjopn  21904  tx1stc  21942  txkgen  21944  xkohaus  21945  xkococnlem  21951  xkoinjcn  21979  ist0-4  22021  kqt0lem  22028  regr1lem2  22032  kqt0  22038  r0sep  22040  nrmr0reg  22041  regr1  22042  kqreg  22043  kqnrm  22044  kqhmph  22111  isfil  22139  filuni  22177  isufil  22195  uffinfix  22219  fmfnfmlem4  22249  hauspwpwf1  22279  alexsublem  22336  alexsubALTlem3  22341  alexsubALTlem4  22342  alexsubALT  22343  ustval  22494  isust  22495  blbas  22723  met1stc  22814  metrest  22817  xrsmopn  23103  cnheibor  23242  itg2cn  24047  jensen  25248  sqff1o  25441  f1otrg  26340  uhgrnbgr0nb  26819  rusgrpropedg  27049  isplig  27944  ispligb  27945  tncp  27946  l2p  27947  eulplig  27953  spanuni  29012  sumdmdii  29883  gsumvsca2  30498  fedgmul  30631  extdg1id  30657  indf1o  30900  gsumesum  30935  dya2iocuni  31158  bnj219  31620  bnj1098  31672  bnj594  31800  bnj580  31801  bnj601  31808  bnj849  31813  bnj996  31843  bnj1006  31847  bnj1029  31854  bnj1033  31855  bnj1090  31865  bnj1110  31868  bnj1124  31874  bnj1128  31876  erdsze  32057  connpconn  32090  rellysconn  32106  cvmsss2  32129  cvmlift2lem12  32169  axextprim  32535  axrepprim  32536  axunprim  32537  axpowprim  32538  axregprim  32539  axinfprim  32540  axacprim  32541  untelirr  32542  untuni  32543  untsucf  32544  unt0  32545  untint  32546  untangtr  32548  dftr6  32594  dffr5  32597  elpotr  32634  dfon2lem3  32638  dfon2lem4  32639  dfon2lem5  32640  dfon2lem6  32641  dfon2lem7  32642  dfon2lem8  32643  dfon2lem9  32644  dfon2  32645  domep  32646  axextdfeq  32651  ax8dfeq  32652  axextdist  32653  axextbdist  32654  exnel  32656  distel  32657  axextndbi  32658  poseq  32704  frrlem4  32735  frrlem8  32739  frrlem10  32741  nosupno  32812  dfiota3  32993  brcup  33009  brcap  33010  dfint3  33022  imagesset  33023  hftr  33252  fness  33306  fneref  33307  neibastop2lem  33317  onsuct0  33398  bj-ax89  33610  bj-elequ12  33611  bj-cleljusti  33612  bj-clabel  33699  bj-el  33703  bj-dtru  33704  bj-dvdemo1  33709  bj-dvdemo2  33710  bj-nfeel2  33748  bj-axc14nf  33749  bj-axc14  33750  bj-ax9  33787  bj-zfauscl  33814  bj-ru0  33824  bj-ru1  33825  bj-ru  33826  currysetlem  33827  curryset  33828  currysetlem1  33829  currysetlem3  33831  currysetALT  33832  bj-nul  33947  bj-nuliota  33948  bj-nuliotaALT  33949  bj-bm1.3ii  33955  bj-elep  33958  finixpnum  34408  fin2solem  34409  fin2so  34410  matunitlindflem1  34419  poimirlem30  34453  poimirlem32  34455  poimir  34456  mblfinlem1  34460  mbfresfi  34469  cnambfre  34471  ftc1anc  34506  ftc2nc  34507  cover2g  34522  sstotbnd2  34584  unichnidl  34841  dfcoels  35206  dfeldisj5  35485  prtlem5  35527  prtlem12  35534  prtlem13  35535  prtlem16  35536  prtlem15  35542  prtlem17  35543  prtlem18  35544  prter1  35546  prter3  35549  ax5el  35604  dveel2ALT  35606  ax12el  35609  pclfinclN  36617  dvh1dim  38109  sn-axrep5v  38638  sn-axprlem3  38639  sn-el  38640  sn-dtru  38641  prjspval  38750  ismrcd1  38780  dford3lem2  39109  dford4  39111  pw2f1ocnv  39119  pw2f1o2  39120  wepwsolem  39127  fnwe2lem2  39136  aomclem8  39146  kelac1  39148  pwslnm  39179  idomsubgmo  39283  intabssd  39370  eu0  39371  ontric3g  39373  alephiso2  39402  inintabss  39423  inintabd  39424  cnvcnvintabd  39445  elintima  39483  dffrege76  39770  frege77  39771  frege89  39783  frege90  39784  frege91  39785  frege93  39787  frege94  39788  frege95  39789  clsk1indlem3  39878  ntrneiel2  39921  ntrneik2  39927  ntrneix2  39928  ntrneik4  39936  gneispa  39965  gneispace2  39967  gneispace3  39968  gneispace  39969  gneispacef  39970  gneispacef2  39971  gneispacern2  39974  gneispace0nelrn  39975  gneispaceel  39978  gneispaceel2  39979  gneispacess  39980  ismnu  40094  mnuop123d  40095  mnussd  40096  mnuop23d  40099  mnupwd  40100  mnuop3d  40104  mnuprdlem4  40108  mnutrd  40113  grumnudlem  40118  ismnuprim  40127  rr-grothprimbi  40128  rr-grothprim  40133  sbcoreleleq  40408  tratrb  40409  ordelordALT  40410  trsbc  40413  truniALT  40414  onfrALTlem5  40415  onfrALTlem4  40416  onfrALTlem3  40417  onfrALTlem2  40419  onfrALTlem1  40421  onfrALT  40422  sspwtrALT  40695  suctrALT2  40710  tratrbVD  40734  truniALTVD  40751  trintALT  40754  onfrALTlem4VD  40759  iota0ndef  42790  aiota0ndef  42811  ralndv1  42820  dfnelbr2  42988  nelbr  42989  nelbrim  42990  sprsymrelf1lem  43135  sprsymrelf  43139  paireqne  43155  dflinc2  43945  lcosslsp  43973  nfintd  44257
  Copyright terms: Public domain W3C validator