MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  elexi Unicode version

Theorem elexi 3119
Description: If a class is a member of another class, it is a set. (Contributed by NM, 11-Jun-1994.)
Hypothesis
Ref Expression
elexi.1
Assertion
Ref Expression
elexi

Proof of Theorem elexi
StepHypRef Expression
1 elexi.1 . 2
2 elex 3118 . 2
31, 2ax-mp 5 1
Colors of variables: wff setvar class
Syntax hints:  e.wcel 1818   cvv 3109
This theorem is referenced by:  onunisuci  4996  mptrabex  6144  caovmo  6512  oev  7183  oe0  7191  oev2  7192  oneo  7249  nnneo  7319  endisj  7624  pwen  7710  sdom1  7739  1sdom  7742  cnfcom2  8167  cnfcom3lem  8168  cnfcom3  8169  cnfcom2OLD  8175  cnfcom3lemOLD  8176  cnfcom3OLD  8177  rankxplim3  8320  pm54.43  8402  mappwen  8514  cda1dif  8577  pm110.643  8578  infcda1  8594  infmap2  8619  ackbij1lem5  8625  cfsuc  8658  isfin4-3  8716  dcomex  8848  pwcfsdom  8979  cfpwsdom  8980  alephom  8981  canthp1lem2  9052  pwxpndom2  9064  inar1  9174  indpi  9306  pinq  9326  archnq  9379  prlem934  9432  0idsr  9495  recexsrlem  9501  supsrlem  9509  opelreal  9528  elreal  9529  elreal2  9530  eqresr  9535  axmulass  9555  ax1ne0  9558  c0ex  9611  1ex  9612  2ex  10632  3ex  10636  pnfex  11351  elxr  11354  xnegex  11436  xaddval  11451  xmulval  11453  om2uzrdg  12067  hashxplem  12491  caucvgr  13498  xpnnenOLD  13943  rpnnen  13960  rexpen  13961  sadcf  14103  sadcp1  14105  phimullem  14309  prmreclem6  14439  xpsc0  14957  xpsc1  14958  xpsfrnel  14960  xpsfrnel2  14962  xpsle  14978  setcepi  15415  efgval  16735  efgi1  16739  frgpuptinv  16789  dmdprdpr  17098  dprdpr  17099  coe1fval3  18247  00ply1bas  18281  ply1plusgfvi  18283  coe1z  18304  coe1mul2  18310  coe1tm  18314  xpstopnlem1  20310  xpstopnlem2  20312  xpsdsval  20884  dscmet  21093  dscopn  21094  icopnfhmeo  21443  iccpnfhmeo  21445  xrhmeo  21446  bndth  21458  mbfimaopnlem  22062  dvef  22381  mdegcl  22469  pige3  22910  cxpval  23045  1cubr  23173  emcllem7  23331  basellem7  23360  prmorcht  23452  sqff1o  23456  ppiublem2  23478  lgsval  23575  lgsdir2lem3  23600  axlowdimlem4  24248  axlowdimlem6  24250  axlowdimlem8  24252  axlowdimlem9  24253  usgraexmpl  24401  usgra2adedgwlkonALT  24616  umgrabi  24983  konigsberg  24987  ex-opab  25153  ex-eprel  25154  ex-id  25155  ex-xp  25157  ex-cnv  25158  ex-dm  25160  ex-rn  25161  ex-res  25162  ex-fv  25164  ex-1st  25165  ex-2nd  25166  hhph  26095  hlim0  26153  hsn0elch  26166  elch0  26172  choc0  26244  shintcli  26247  shincli  26280  chincli  26378  h1deoi  26467  h1de2bi  26472  h1de2ctlem  26473  spansni  26475  df0op2  26671  ho01i  26747  nmop0h  26910  opsqrlem2  27060  opsqrlem4  27062  opsqrlem5  27063  hmopidmchi  27070  atoml2i  27302  xrge0iifhmeo  27918  rezh  27952  rrhre  27999  sxbrsigalem5  28259  ballotth  28476  subfacp1lem3  28626  subfacp1lem5  28628  kur14lem7  28656  kur14lem9  28658  mrsubcv  28870  mrsubrn  28873  mvhf1  28919  msubvrs  28920  nofv  29417  sltres  29424  noxp1o  29426  noxp2o  29427  bdayfo  29435  nobndlem3  29454  nobndlem7  29458  nobndup  29460  nobnddown  29461  onsucsuccmpi  29908  mbfresfi  30061  fdc  30238  rabren3dioph  30749  pw2f1ocnv  30979  cxpcncf2  31703  wallispilem2  31848  stirlinglem14  31869  fourierdlem70  31959  fourierdlem83  31972  fourierdlem102  31991  fourierdlem103  31992  fourierdlem104  31993  fourierdlem114  32003  fouriersw  32014  bnj1015  34019  cllem0  37751  trclub  37784  trclubg  37785  frege56c  37946
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-12 1854  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-v 3111
  Copyright terms: Public domain W3C validator