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

Theorem elex 2973
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 1603 . 2  |-  ( E. x ( x  =  A  /\  x  e.  B )  ->  E. x  x  =  A )
2 df-clel 2439 . 2  |-  ( A  e.  B  <->  E. x
( x  =  A  /\  x  e.  B
) )
3 isset 2969 . 2  |-  ( A  e.  _V  <->  E. x  x  =  A )
41, 2, 33imtr4i 259 1  |-  ( A  e.  B  ->  A  e.  _V )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360   E.wex 1551    = wceq 1654    e. wcel 1728   _Vcvv 2965
This theorem is referenced by:  elexi  2974  elisset  2975  vtoclgft  3011  vtoclgf  3019  vtocl2gf  3022  vtocl3gf  3023  spcimgft  3036  elab4g  3095  elrabf  3100  mob  3125  sbcex  3179  sbcel1v  3233  sbcrextOLD  3250  sbcabel  3257  csbiebt  3289  eldif  3319  ssv  3357  elun  3477  elin  3519  csbcomgOLD  3668  csbnestgf  3670  sbcco3g  3674  csbco3g  3676  csbidmgOLD  3679  csbvarg  3680  sbccsb2  3683  snidb  3869  ifpr  3885  dfopg  4011  eluni  4047  eliun  4126  csbexg  4371  csbexgOLD  4373  nvel  4377  class2seteq  4403  axpweq  4411  elopab  4497  epelg  4530  elon2  4627  ordsssuc2  4705  unexg  4745  reusv2lem4  4762  reuhypd  4785  elpwun  4791  ordeleqon  4804  ssonprc  4807  onintrab  4816  sucexg  4825  ordsucelsuc  4837  onzsl  4861  opelvvg  4958  opeliunxp2  5048  ideqg  5059  elrnmptg  5155  imasng  5261  elimasni  5266  iniseg  5270  elxp5  5393  dmmptg  5402  iota2  5479  fnmpt  5606  elfvex  5789  fvelimab  5818  fvmptdf  5852  fvmptdv2  5854  mpteqb  5855  fvmptt  5856  fvmptf  5857  fvopab6  5862  fprg  5951  eloprabga  6196  ovmpt2s  6233  ov2gf  6234  ovmpt2dxf  6235  ovmpt2x  6238  ovmpt2ga  6239  ovmpt2df  6241  suppssfv  6337  suppssov1  6338  offval3  6354  releldm2  6433  fnmpt2  6455  mpt2exg  6459  brtpos2  6521  brrpssg  6560  sorpssi  6564  fvopab5  6570  pwuninel  6581  undefval  6582  riotasv2d  6630  riotasv2dOLD  6631  riotasv3d  6634  riotasv3dOLD  6635  tfr2b  6693  tz7.49  6738  oeordi  6866  oeeu  6882  relelec  6981  ecdmn0  6983  mapvalg  7064  pmvalg  7065  elpmg  7068  elixp2  7102  mptelixpg  7135  elixpsn  7137  2pwuninel  7298  pwfi  7438  fival  7453  elfi2  7455  dffi2  7464  elfiun  7471  wemappo  7554  wemapso  7556  wemapso2  7557  harval  7566  brwdom  7571  fowdom  7575  brwdom2  7577  brwdom3  7586  en2lp  7607  cantnfsuc  7661  cnfcomlem  7692  rankvalb  7759  pwwf  7769  rankwflem  7777  rankr1g  7794  r1pw  7807  r1pwOLD  7808  r1rankid  7821  cardval3  7877  pm54.43lem  7924  dfac8alem  7948  ac5num  7955  isacn  7963  numacn  7968  acndom  7970  cardinfima  8016  unialeph  8020  cdaval  8088  cflm  8168  isfin3  8214  isf32lem2  8272  isfin1-2  8303  itunifval  8334  numth3  8388  ttukeylem1  8427  ttukeylem3  8429  cardidg  8461  ondomon  8476  canth4  8560  canthnumlem  8561  canthwelem  8563  elwina  8599  elina  8600  wuncval  8655  grothpw  8739  tskmval  8752  eltskm  8756  recmulnq  8879  elnp  8902  elnpi  8903  npomex  8911  lbinfm  9999  elfzp12  11164  seqp1  11376  seqf1olem2  11401  hashinf  11661  hashnn0pnf  11664  hashxrcl  11678  hashbclem  11739  iswrd  11767  ccatfval  11780  swrdval  11802  splval  11818  splcl  11819  cats1un  11828  revval  11830  limsupcl  12305  limsupval  12306  clim  12326  rlim  12327  fsumrlim  12628  hashbcval  13408  isstruct2  13516  strfvnd  13522  setsvalg  13530  setscom  13535  strfv2d  13537  setsid  13546  ressval  13554  ressinbas  13563  restval  13692  prdsval  13716  prdssca  13717  pwsval  13746  imasval  13775  divsval  13805  xpsfrnel  13826  xpsfrnel2  13828  xpsval  13835  ismre  13853  oppcval  13977  brssc  14052  rescval  14065  issubc  14073  isfunc  14099  cofuval  14117  resfval  14127  funcres2c  14136  homadm  14233  homacd  14234  setcval  14270  catcval  14289  xpcval  14312  prfval  14334  curfval  14358  uncfval  14369  pltfval  14454  pospo  14468  lubfval  14473  glbfval  14478  joinfval  14482  meetfval  14489  p0val  14508  p1val  14509  pospropd  14599  oduclatb  14609  ipoval  14618  ipodrsima  14629  spwval2  14694  prdsmndd  14766  prds0g  14767  pws0g  14769  gsumvalx  14812  frmdval  14834  vrmdfval  14839  prdsgrpd  14965  prdsinvgd  14966  eqgfval  15026  eqgval  15027  gaid  15114  symgval  15132  elsymgbas  15135  cntzfval  15157  gexval  15250  sylow2a  15291  lsmfval  15310  pj1fval  15364  frgpval  15428  vrgpfval  15436  prdscmnd  15514  dmdprd  15597  dprdw  15606  pws1  15760  pwsmgp  15762  dvdsr  15789  isunit  15800  isirred  15842  issrng  15976  lssset  16048  prdslmodd  16083  lspfval  16087  islbs  16186  sraval  16286  psrval  16467  mvrfval  16522  ltbval  16570  opsrval  16573  coe1fval  16641  zlmval  16835  ocvfval  16931  cssval  16947  thlval  16960  eltopspOLD  17021  istpsOLD  17023  basdif0  17056  tgval  17058  eltg  17060  eltg2  17061  neipeltop  17231  islp  17242  ordtval  17291  dis2ndc  17561  txval  17634  qtopval  17765  elmptrab2  17898  isfbas  17899  isfildlem  17927  snfil  17934  cfinfil  17963  csdfil  17964  supfil  17965  numufl  17985  fin1aufil  18002  fmval  18013  fmf  18015  isfcls  18079  alexsub  18114  alexsubb  18115  tsmsfbas  18195  tsmsval2  18197  elutop  18301  isusp  18329  ispsmet  18373  ismet  18391  isxmet  18392  prdsdsf  18435  prdsxmet  18437  blfvalps  18451  metustelOLD  18619  metustel  18620  tngval  18718  elpi1  19108  itgfsum  19754  evlsrhm  19980  evlssca  19981  evlsvar  19982  q1peqb  20115  ig1pval  20133  taylfval  20313  ulmval  20334  mtest  20358  cusgrafilem1  21526  isuvtx  21535  wlks  21564  wlkon  21568  trls  21574  trlon  21578  2trllemA  21588  pths  21604  spths  21605  pthon  21613  spthon  21620  2wlklem1  21635  crcts  21647  cycls  21648  vdgrfval  21704  avril1  21795  gidval  21839  elghomlem2  21988  isrngo  22004  isdivrngo  22057  isvc  22098  0vfval  22123  elunop  23413  rabexgfGS  24023  disjdifprg  24052  disjdifprg2  24053  fmptpr  24097  abfmpunirn  24099  rabfmpunirn  24100  fnmptf  24109  funcnvmptOLD  24117  funcnvmpt  24118  inftmrel  24285  isinftm  24286  isarchi  24287  qqhval2  24401  rrhval  24414  xrhval  24419  indv  24445  esumc  24481  esumpcvgval  24503  ofcfval  24516  ofcfval3  24520  issiga  24529  baselsiga  24533  sigasspw  24534  issgon  24541  isrnsigau  24545  sigagenval  24558  cldssbrsiga  24576  sxval  24579  ismeas  24588  cnmbfm  24648  mbfmcnt  24653  sitgval  24682  sitmval  24696  orvcval  24750  orvcval4  24753  ballotlemsv  24802  relexpsucr  25165  eldm3  25420  opelco3  25438  elima4  25439  wsuclem  25611  elno  25636  nobndlem8  25689  nobndup  25690  nobnddown  25691  elfix2  25784  elsingles  25798  fvimage  25811  funpartlem  25822  elaltxp  25855  brcolinear2  26027  ellines  26121  limsucncmpi  26230  findabrcl  26239  topfneec  26413  topfneec2  26414  islocfin  26418  fnejoin2  26440  opelopab3  26460  elrfi  26860  nacsfix  26878  mapfzcons2  26887  sbc2rexg  26956  sbc4rexg  26957  setindtrs  27208  wepwso  27229  inisegn0  27230  dsmmval  27289  dsmmbase  27290  frlmval  27305  uvcfval  27322  elfilspd  27344  islinds  27368  hbtlem1  27416  hbtlem7  27418  rgspnval  27462  pmtrfval  27482  symggen  27500  mamufval  27532  matval  27554  mendval  27580  addrval  27759  subrval  27760  mulvval  27761  dvcosre  27829  itgsinexplem1  27836  stoweidlem26  27863  stoweidlem35  27872  stirlinglem14  27924  afvprc  28096  lswrd  28391  wwlk  28461  wwlkn  28462  is2wlkonot  28493  is2spthonot  28494  2wlksot  28497  2spthsot  28498  usgreghash2spot  28630  bnj1463  29598  lshpset  29950  lsatset  29962  lcvfbr  29992  lflset  30031  lkrfval  30059  lkrval2  30062  islshpkrN  30092  ldualset  30097  cmtfvalN  30182  cvrfval  30240  pats  30257  llnset  30476  lplnset  30500  lvolset  30543  lineset  30709  pointsetN  30712  psubspset  30715  pmapfval  30727  paddfval  30768  pclfvalN  30860  polfvalN  30875  psubclsetN  30907  watfvalN  30963  lhpset  30966  lautset  31053  pautsetN  31069  ldilfset  31079  ltrnfset  31088  dilfsetN  31123  trnfsetN  31126  trlfset  31131  tgrpfset  31715  tendofset  31729  erngfset  31770  erngfset-rN  31778  dvafset  31975  diaffval  32002  dvhfset  32052  docaffvalN  32093  djaffvalN  32105  dibffval  32112  dicffval  32146  dihffval  32202  dochffval  32321  djhffval  32368  lpolsetN  32454  lcdfval  32560  mapdffval  32598  hvmapffval  32730  hdmap1ffval  32768  hdmapffval  32801  hgmapffval  32860  hlhilset  32909
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1628  ax-9 1669  ax-8 1690  ax-11 1764  ax-ext 2424
This theorem depends on definitions:  df-bi 179  df-an 362  df-ex 1552  df-sb 1661  df-clab 2430  df-cleq 2436  df-clel 2439  df-v 2967
  Copyright terms: Public domain W3C validator