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

Theorem elex 2907
Description: If a class is a member of another class, it is a set. Theorem 6.12 of [Quine] p. 44. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 8-Jun-2011.)
Assertion
Ref Expression
elex  |-  ( A  e.  B  ->  A  e.  _V )

Proof of Theorem elex
Dummy variable  x is distinct from all other variables.
StepHypRef Expression
1 exsimpl 1599 . 2  |-  ( E. x ( x  =  A  /\  x  e.  B )  ->  E. x  x  =  A )
2 df-clel 2383 . 2  |-  ( A  e.  B  <->  E. x
( x  =  A  /\  x  e.  B
) )
3 isset 2903 . 2  |-  ( A  e.  _V  <->  E. x  x  =  A )
41, 2, 33imtr4i 258 1  |-  ( A  e.  B  ->  A  e.  _V )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359   E.wex 1547    = wceq 1649    e. wcel 1717   _Vcvv 2899
This theorem is referenced by:  elexi  2908  elisset  2909  vtoclgft  2945  vtoclgf  2953  vtocl2gf  2956  vtocl3gf  2957  spcimgft  2970  elab4g  3029  elrabf  3034  mob  3059  sbcex  3113  sbcrext  3177  sbcabel  3181  csbexg  3204  csbcomg  3217  csbvarg  3221  csbiebt  3230  csbnestgf  3242  csbidmg  3247  sbcco3g  3248  csbco3g  3250  eldif  3273  ssv  3311  elun  3431  elin  3473  snidb  3783  ifpr  3799  dfopg  3924  eluni  3960  eliun  4039  nvel  4283  class2seteq  4309  axpweq  4317  elopab  4403  epelg  4436  elon2  4533  ordsssuc2  4610  unexg  4650  reusv2lem4  4667  reuhypd  4690  elpwun  4696  ordeleqon  4709  ssonprc  4712  onintrab  4721  sucexg  4730  ordsucelsuc  4742  onzsl  4766  opelvvg  4863  opeliunxp2  4953  ideqg  4964  elrnmptg  5060  imasng  5166  elimasni  5171  iniseg  5175  elxp5  5298  dmmptg  5307  iota2  5384  fnmpt  5511  elfvex  5698  fvelimab  5721  fvmptdf  5755  fvmptdv2  5757  mpteqb  5758  fvmptt  5759  fvmptf  5760  fvopab6  5765  fprg  5854  eloprabga  6099  ovmpt2s  6136  ov2gf  6137  ovmpt2dxf  6138  ovmpt2x  6141  ovmpt2ga  6142  ovmpt2df  6144  suppssfv  6240  suppssov1  6241  offval3  6257  releldm2  6336  fnmpt2  6358  mpt2exg  6362  brtpos2  6421  brrpssg  6460  sorpssi  6464  fvopab5  6470  pwuninel  6481  undefval  6482  riotasv2d  6530  riotasv2dOLD  6531  riotasv3d  6534  riotasv3dOLD  6535  tfr2b  6593  tz7.49  6638  oeordi  6766  oeeu  6782  relelec  6881  ecdmn0  6883  mapvalg  6964  pmvalg  6965  elpmg  6968  elixp2  7002  mptelixpg  7035  elixpsn  7037  2pwuninel  7198  pwfi  7337  fival  7352  elfi2  7354  dffi2  7363  elfiun  7370  wemappo  7451  wemapso  7453  wemapso2  7454  harval  7463  brwdom  7468  fowdom  7472  brwdom2  7474  brwdom3  7483  en2lp  7504  cantnfsuc  7558  cnfcomlem  7589  rankvalb  7656  pwwf  7666  rankwflem  7674  rankr1g  7691  r1pw  7704  r1pwOLD  7705  r1rankid  7718  cardval3  7772  pm54.43lem  7819  dfac8alem  7843  ac5num  7850  isacn  7858  numacn  7863  acndom  7865  cardinfima  7911  unialeph  7915  cdaval  7983  cflm  8063  isfin3  8109  isf32lem2  8167  isfin1-2  8198  itunifval  8229  numth3  8283  ttukeylem1  8322  ttukeylem3  8324  cardidg  8356  ondomon  8371  canth4  8455  canthnumlem  8456  canthwelem  8458  elwina  8494  elina  8495  wuncval  8550  grothpw  8634  tskmval  8647  eltskm  8651  recmulnq  8774  elnp  8797  elnpi  8798  npomex  8806  lbinfm  9893  elfzp12  11056  seqp1  11265  seqf1olem2  11290  hashinf  11550  hashnn0pnf  11553  hashxrcl  11567  hashbclem  11628  iswrd  11656  ccatfval  11669  swrdval  11691  splval  11707  splcl  11708  cats1un  11717  revval  11719  limsupcl  12194  limsupval  12195  clim  12215  rlim  12216  fsumrlim  12517  hashbcval  13297  isstruct2  13405  strfvnd  13411  setsvalg  13419  setscom  13424  strfv2d  13426  setsid  13435  ressval  13443  ressinbas  13452  restval  13581  prdsval  13605  prdssca  13606  pwsval  13635  imasval  13664  divsval  13694  xpsfrnel  13715  xpsfrnel2  13717  xpsval  13724  ismre  13742  oppcval  13866  brssc  13941  rescval  13954  issubc  13962  isfunc  13988  cofuval  14006  resfval  14016  funcres2c  14025  homadm  14122  homacd  14123  setcval  14159  catcval  14178  xpcval  14201  prfval  14223  curfval  14247  uncfval  14258  pltfval  14343  pospo  14357  lubfval  14362  glbfval  14367  joinfval  14371  meetfval  14378  p0val  14397  p1val  14398  pospropd  14488  oduclatb  14498  ipoval  14507  ipodrsima  14518  spwval2  14583  prdsmndd  14655  prds0g  14656  pws0g  14658  gsumvalx  14701  frmdval  14723  vrmdfval  14728  prdsgrpd  14854  prdsinvgd  14855  eqgfval  14915  eqgval  14916  gaid  15003  symgval  15021  elsymgbas  15024  cntzfval  15046  gexval  15139  sylow2a  15180  lsmfval  15199  pj1fval  15253  frgpval  15317  vrgpfval  15325  prdscmnd  15403  dmdprd  15486  dprdw  15495  pws1  15649  pwsmgp  15651  dvdsr  15678  isunit  15689  isirred  15731  issrng  15865  lssset  15937  prdslmodd  15972  lspfval  15976  islbs  16075  sraval  16175  psrval  16356  mvrfval  16411  ltbval  16459  opsrval  16462  coe1fval  16530  zlmval  16720  ocvfval  16816  cssval  16832  thlval  16845  eltopspOLD  16906  istpsOLD  16908  basdif0  16941  tgval  16943  eltg  16945  eltg2  16946  neipeltop  17116  islp  17127  ordtval  17175  dis2ndc  17444  txval  17517  qtopval  17648  elmptrab2  17781  isfbas  17782  isfildlem  17810  snfil  17817  cfinfil  17846  csdfil  17847  supfil  17848  numufl  17868  fin1aufil  17885  fmval  17896  fmf  17898  isfcls  17962  alexsub  17997  alexsubb  17998  tsmsfbas  18078  tsmsval2  18080  elutop  18184  isusp  18212  ismet  18262  isxmet  18263  prdsdsf  18305  prdsxmet  18307  metustel  18470  tngval  18551  elpi1  18941  itgfsum  19585  evlsrhm  19809  evlssca  19810  evlsvar  19811  q1peqb  19944  ig1pval  19962  taylfval  20142  ulmval  20163  mtest  20187  cusgrafilem1  21354  isuvtx  21363  wlks  21390  wlkon  21394  trls  21400  trlon  21404  pths  21420  spths  21421  pthon  21429  crcts  21457  cycls  21458  vdgrfval  21514  avril1  21605  gidval  21649  elghomlem2  21798  isrngo  21814  isdivrngo  21867  isvc  21908  0vfval  21933  elunop  23223  rabexgfGS  23831  disjdifprg  23861  disjdifprg2  23862  fmptpr  23904  abfmpunirn  23906  rabfmpunirn  23907  fnmptf  23916  funcnvmptOLD  23923  funcnvmpt  23924  qqhval2  24165  rrhval  24178  indv  24206  esumc  24242  esumpcvgval  24264  ofcfval  24277  ofcfval3  24281  issiga  24290  baselsiga  24294  sigasspw  24295  issgon  24302  isrnsigau  24306  sigagenval  24319  cldssbrsiga  24337  sxval  24340  ismeas  24349  cnmbfm  24407  mbfmcnt  24412  orvcval  24494  orvcval4  24497  ballotlemsv  24546  relexpsucr  24909  eldm3  25143  elno  25324  nobndlem8  25377  nobndup  25378  nobnddown  25379  elfix2  25468  elsingles  25481  fvimage  25494  funpartlem  25505  elaltxp  25534  brcolinear2  25706  ellines  25800  limsucncmpi  25909  findabrcl  25918  topfneec  26062  topfneec2  26063  islocfin  26067  fnejoin2  26089  opelopab3  26109  elrfi  26439  nacsfix  26457  mapfzcons2  26466  sbc2rexg  26535  sbc4rexg  26536  setindtrs  26787  wepwso  26808  inisegn0  26809  dsmmval  26869  dsmmbase  26870  frlmval  26885  uvcfval  26902  elfilspd  26924  islinds  26948  hbtlem1  26996  hbtlem7  26998  rgspnval  27042  pmtrfval  27062  symggen  27080  mamufval  27112  matval  27134  mendval  27160  addrval  27339  subrval  27340  mulvval  27341  dvcosre  27409  itgsinexplem1  27416  stoweidlem26  27443  stoweidlem35  27452  stirlinglem14  27504  afvprc  27677  bnj1463  28762  lshpset  29093  lsatset  29105  lcvfbr  29135  lflset  29174  lkrfval  29202  lkrval2  29205  islshpkrN  29235  ldualset  29240  cmtfvalN  29325  cvrfval  29383  pats  29400  llnset  29619  lplnset  29643  lvolset  29686  lineset  29852  pointsetN  29855  psubspset  29858  pmapfval  29870  paddfval  29911  pclfvalN  30003  polfvalN  30018  psubclsetN  30050  watfvalN  30106  lhpset  30109  lautset  30196  pautsetN  30212  ldilfset  30222  ltrnfset  30231  dilfsetN  30266  trnfsetN  30269  trlfset  30274  tgrpfset  30858  tendofset  30872  erngfset  30913  erngfset-rN  30921  dvafset  31118  diaffval  31145  dvhfset  31195  docaffvalN  31236  djaffvalN  31248  dibffval  31255  dicffval  31289  dihffval  31345  dochffval  31464  djhffval  31511  lpolsetN  31597  lcdfval  31703  mapdffval  31741  hvmapffval  31873  hdmap1ffval  31911  hdmapffval  31944  hgmapffval  32003  hlhilset  32052
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-11 1753  ax-ext 2368
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1548  df-sb 1656  df-clab 2374  df-cleq 2380  df-clel 2383  df-v 2901
  Copyright terms: Public domain W3C validator