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

Theorem elex 3118
Description: If a class is a member of another class, it is a set. Theorem 6.12 of [Quine] p. 44. (Contributed by NM, 26-May-1993.) (Proof shortened by Andrew Salmon, 8-Jun-2011.)
Assertion
Ref Expression
elex

Proof of Theorem elex
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 exsimpl 1677 . 2
2 df-clel 2452 . 2
3 isset 3113 . 2
41, 2, 33imtr4i 266 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369  =wceq 1395  E.wex 1612  e.wcel 1818   cvv 3109
This theorem is referenced by:  elexi  3119  elisset  3120  vtoclgft  3157  vtoclgf  3165  vtoclg1f  3166  vtocl2gf  3169  vtocl3gf  3170  spcimgft  3185  elab4g  3250  elrabf  3255  mob  3281  sbcex  3337  sbcel1v  3392  sbcrextOLD  3409  sbcabel  3416  csbiebt  3454  eldif  3485  ssv  3523  elun  3644  elin  3686  csbcomgOLD  3838  csbnestgf  3840  sbcco3g  3843  csbco3g  3844  csbidmgOLD  3847  csbvarg  3848  sbccsb2  3851  snidb  4056  ifpr  4077  eldifvsn  4162  dfopg  4215  eluni  4252  eliun  4335  csbexg  4584  csbexgOLD  4586  nvel  4591  class2seteq  4620  axpweq  4629  reusv2lem4  4656  reuhypd  4679  elopab  4760  epelg  4797  elon2  4894  ordsssuc2  4971  opelvvg  5050  opeliunxp2  5146  ideqg  5159  elrnmptg  5257  imasng  5364  elimasni  5369  iniseg  5373  dmmptg  5509  iota2  5582  fnmpt  5712  dmmptd  5716  elfvex  5898  fvelimab  5929  fvmptdf  5967  fvmptdv2  5969  mpteqb  5970  fvmptt  5971  fvmptf  5972  fvopab5  5979  fvopab6  5980  fprg  6080  fmptpr  6096  eloprabga  6389  ovmpt2s  6426  ov2gf  6427  ovmpt2dxf  6428  ovmpt2x  6431  ovmpt2ga  6432  ovmpt2df  6434  suppssfvOLD  6531  suppssov1OLD  6532  ovmpt3rab1  6534  brrpssg  6582  sorpssi  6586  unexg  6601  elpwun  6613  ordeleqon  6624  ssonprc  6627  onintrab  6636  sucexg  6645  ordsucelsuc  6657  onzsl  6681  elxp5  6745  offval3  6794  releldm2  6850  fnmpt2  6868  mpt2exg  6875  offval22  6879  suppval  6920  mptsuppd  6942  suppssov1  6951  suppssfv  6955  brtpos2  6980  pwuninel  7023  undefval  7024  tfr2b  7084  tz7.49  7129  oeordi  7255  oeeu  7271  relelec  7371  ecdmn0  7373  mapvalg  7449  pmvalg  7450  elpmg  7454  elixp2  7493  mptelixpg  7526  elixpsn  7528  2pwuninel  7692  pwfi  7835  fival  7892  elfi2  7894  dffi2  7903  elfiun  7910  wemappo  7995  wemapso  7997  wemapso2OLD  7998  wemapso2lem  7999  harval  8009  brwdom  8014  fowdom  8018  brwdom2  8020  brwdom3  8029  en2lp  8051  cantnfsuc  8110  cantnfsucOLD  8140  cnfcomlem  8164  cnfcomlemOLD  8172  rankvalb  8236  pwwf  8246  rankwflem  8254  rankr1g  8271  r1pw  8284  r1pwOLD  8285  r1rankid  8298  cardval3  8354  pm54.43lem  8401  dfac8alem  8431  ac5num  8438  isacn  8446  numacn  8451  acndom  8453  cardinfima  8499  unialeph  8503  cdaval  8571  cflm  8651  isfin3  8697  isf32lem2  8755  isfin1-2  8786  itunifval  8817  numth3  8871  ttukeylem1  8910  ttukeylem3  8912  cardidg  8944  ondomon  8959  canth4  9046  canthnumlem  9047  canthwelem  9049  elwina  9085  elina  9086  wuncval  9141  grothpw  9225  tskmval  9238  eltskm  9242  recmulnq  9363  elnp  9386  elnpi  9387  npomex  9395  lbinfm  10521  elfzp12  11786  mptnn0fsupp  12103  mptnn0fsuppr  12105  seqp1  12122  seqf1olem2  12147  hashinf  12410  hashnn0pnf  12415  hashxrcl  12429  hashbclem  12501  iswrd  12550  lsw  12585  ccatfval  12592  swrdval  12644  cats1un  12701  splval  12727  splcl  12728  revval  12734  reps  12742  limsupcl  13296  limsupval  13297  clim  13317  rlim  13318  fsumrlim  13625  hashbcval  14520  isstruct2  14641  strfvnd  14647  setsvalg  14655  setscom  14662  strfv2d  14664  setsid  14673  ressval  14684  ressinbas  14693  restval  14824  prdsval  14852  prdssca  14853  pwsval  14883  imasval  14908  qusval  14939  xpsfrnel  14960  xpsfrnel2  14962  xpsval  14969  ismre  14987  oppcval  15108  brssc  15183  rescval  15196  issubc  15204  isfunc  15233  cofuval  15251  resfval  15261  funcres2c  15270  homadm  15367  homacd  15368  setcval  15404  catcval  15423  xpcval  15446  prfval  15468  curfval  15492  uncfval  15503  pltfval  15589  pospo  15603  lubfval  15608  glbfval  15621  joinfval  15631  meetfval  15645  p0val  15671  p1val  15672  pospropd  15764  oduclatb  15774  ipoval  15784  ipodrsima  15795  gsumvalx  15897  prdsmndd  15953  prds0g  15954  pws0g  15956  frmdval  16019  vrmdfval  16024  prdsgrpd  16179  prdsinvgd  16180  eqgfval  16249  eqgval  16250  gaid  16337  cntzfval  16358  symgval  16404  elsymgbas  16407  symg2hash  16422  pmtrfval  16475  symggen  16495  gexval  16598  lsmfval  16658  pj1fval  16712  frgpval  16776  vrgpfval  16784  prdscmnd  16867  dmdprd  17029  dprdw  17043  dprdwOLD  17050  pws1  17265  pwsmgp  17267  dvdsr  17295  isunit  17306  isirred  17348  isrim0  17372  issrng  17499  lssset  17580  prdslmodd  17615  lspfval  17619  islbs  17722  sraval  17822  psrval  18011  mvrfval  18076  ltbval  18136  opsrval  18139  evlsrhm  18190  evlssca  18191  evlsvar  18192  coe1fval  18244  evls1fval  18356  zlmval  18553  psgnevpmb  18623  ocvfval  18697  cssval  18713  thlval  18726  dsmmval  18765  dsmmbase  18766  frlmval  18779  uvcfval  18815  elfilspd  18838  islinds  18844  mamufval  18887  matval  18913  oftpos  18954  dmatval  18994  scmatval  19006  mvmulfval  19044  smadiadetglem2  19174  cpmat  19210  mat2pmatfval  19224  cpm2mfval  19250  decpmatval0  19265  pm2mpval  19296  chpmatfval  19331  eltopspOLD  19419  istpsOLD  19421  basdif0  19454  tgval  19456  eltg  19458  eltg2  19459  neipeltop  19630  islp  19641  ordtval  19690  dis2ndc  19961  islocfin  20018  txval  20065  qtopval  20196  elmptrab2  20329  isfbas  20330  isfildlem  20358  snfil  20365  cfinfil  20394  csdfil  20395  supfil  20396  numufl  20416  fin1aufil  20433  fmval  20444  fmf  20446  isfcls  20510  alexsub  20545  alexsubb  20546  tsmsfbas  20626  tsmsval2  20628  elutop  20736  isusp  20764  ispsmet  20808  ismet  20826  isxmet  20827  prdsdsf  20870  prdsxmet  20872  blfvalps  20886  metustelOLD  21054  metustel  21055  tngval  21153  elpi1  21545  rrxval  21819  itgfsum  22233  q1peqb  22555  ig1pval  22573  taylfval  22754  ulmval  22775  mtest  22799  iscgrg  23904  isismt  23921  legval  23971  mirval  24036  israg  24074  perpln1  24087  perpln2  24088  isperp  24089  ishpg  24128  midf  24142  ismidb  24144  lmif  24151  islmib  24153  iscgra  24169  f1otrg  24174  f1otrge  24175  ttgval  24178  xmstrkgc  24189  edgval  24339  cusgrafilem1  24479  isuvtx  24488  wlks  24519  wlkon  24533  trls  24538  trlon  24542  2trllemA  24552  pths  24568  spths  24569  pthon  24577  spthon  24584  2wlklem1  24599  crcts  24622  cycls  24623  wwlk  24681  wwlkn  24682  wlknwwlknsur  24712  clwlk  24753  clwwlk  24766  clwwlkn  24767  is2wlkonot  24863  is2spthonot  24864  2wlksot  24867  2spthsot  24868  vdgrfval  24895  usgreghash2spot  25069  avril1  25171  gidval  25215  elghomlem2OLD  25364  isrngo  25380  isdivrngo  25433  isvc  25474  0vfval  25499  elunop  26791  rabexgfGS  27401  disjdifprg  27436  disjdifprg2  27437  abfmpunirn  27490  rabfmpunirn  27491  fnmptf  27500  funcnvmptOLD  27509  funcnvmpt  27510  fcobijfs  27549  sgnsv  27717  inftmrel  27724  isinftm  27725  resvval  27817  ispcmp  27860  qqhval2  27963  rrhval  27977  xrhval  27996  indv  28026  esumc  28062  esumpcvgval  28084  ofcfval  28097  ofcfval3  28101  issiga  28111  baselsiga  28115  sigasspw  28116  issgon  28123  isrnsigau  28127  sigagenval  28140  cldssbrsiga  28158  sxval  28161  ismeas  28170  cnmbfm  28234  mbfmcnt  28239  oms0  28266  omsmon  28267  sitgval  28274  sitmval  28290  eulerpartlemt0  28308  sseqval  28327  sseqmw  28330  sseqp1  28334  orvcval  28396  orvcval4  28399  ballotlemsv  28448  mrexval  28861  mrsubffval  28867  msubffval  28883  mclsval  28923  relexpsucr  29053  eldm3  29191  opelco3  29208  elima4  29209  wsuclem  29381  elno  29406  nobndlem8  29459  nobndup  29460  nobnddown  29461  elfix2  29554  elsingles  29568  fvimage  29581  funpartlem  29592  elaltxp  29625  brcolinear2  29708  ellines  29802  limsucncmpi  29910  findabrcl  29919  topfneec  30173  topfneec2  30174  fnejoin2  30187  opelopab3  30207  elrfi  30626  nacsfix  30644  mapfzcons2  30651  sbc2rexgOLD  30721  sbc4rexgOLD  30723  setindtrs  30967  wepwso  30988  inisegn0  30989  hbtlem1  31072  hbtlem7  31074  rgspnval  31117  mendval  31132  addrval  31375  subrval  31376  mulvval  31377  upbdrech  31505  climf  31628  dvcosre  31706  itgsinexplem1  31752  itgsubsticclem  31774  stoweidlem26  31808  stoweidlem35  31817  stirlinglem14  31869  fourierdlem42  31931  fourierdlem81  31970  fourierdlem89  31978  fourierdlem91  31980  afvprc  32229  vtxval  32383  gordval  32388  gsizval  32389  intopval  32526  clintopval  32528  assintopval  32529  tpres  32554  estrcval  32630  estrres  32645  isrngisom  32702  rngcvalOLD  32769  rngcval  32770  rnghmsscmap  32782  ringcvalOLD  32815  ringcval  32816  rhmsscmap  32828  dmatbas  33004  lincop  33009  lcoop  33012  bnj1463  34111  bj-sngltag  34541  bj-xtagex  34547  bj-diagval  34605  bj-eldiag2  34607  riotasv2d  34688  riotasv3d  34691  lshpset  34703  lsatset  34715  lcvfbr  34745  lflset  34784  lkrfval  34812  lkrval2  34815  islshpkrN  34845  ldualset  34850  cmtfvalN  34935  cvrfval  34993  pats  35010  llnset  35229  lplnset  35253  lvolset  35296  lineset  35462  pointsetN  35465  psubspset  35468  pmapfval  35480  paddfval  35521  pclfvalN  35613  polfvalN  35628  psubclsetN  35660  watfvalN  35716  lhpset  35719  lautset  35806  pautsetN  35822  ldilfset  35832  ltrnfset  35841  dilfsetN  35877  trnfsetN  35880  trlfset  35885  tgrpfset  36470  tendofset  36484  erngfset  36525  erngfset-rN  36533  dvafset  36730  diaffval  36757  dvhfset  36807  docaffvalN  36848  djaffvalN  36860  dibffval  36867  dicffval  36901  dihffval  36957  dochffval  37076  djhffval  37123  lpolsetN  37209  lcdfval  37315  mapdffval  37353  hvmapffval  37485  hdmap1ffval  37523  hdmapffval  37556  hgmapffval  37615  hlhilset  37664
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