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

Theorem elex 2809
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 1582 . 2  |-  ( E. x ( x  =  A  /\  x  e.  B )  ->  E. x  x  =  A )
2 df-clel 2292 . 2  |-  ( A  e.  B  <->  E. x
( x  =  A  /\  x  e.  B
) )
3 isset 2805 . 2  |-  ( A  e.  _V  <->  E. x  x  =  A )
41, 2, 33imtr4i 257 1  |-  ( A  e.  B  ->  A  e.  _V )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358   E.wex 1531    = wceq 1632    e. wcel 1696   _Vcvv 2801
This theorem is referenced by:  elexi  2810  elisset  2811  vtoclgft  2847  vtoclgf  2855  vtocl2gf  2858  vtocl3gf  2859  spcimgft  2872  elab4g  2931  elrabf  2935  mob  2960  sbcex  3013  sbcieg  3036  sbcrext  3077  sbcabel  3081  csbexg  3104  csbcomg  3117  csbvarg  3121  csbiebt  3130  csbnestgf  3142  csbidmg  3148  sbcco3g  3149  csbco3g  3151  eldif  3175  ssv  3211  elun  3329  elin  3371  snidb  3679  ifpr  3694  dfopg  3810  eluni  3846  eliun  3925  nvel  4169  class2seteq  4195  axpweq  4203  elopab  4288  epelg  4322  elon2  4419  ordsssuc2  4497  unexg  4537  reusv2lem4  4554  reuhypd  4577  elpwun  4583  ordeleqon  4596  ssonprc  4599  onintrab  4608  sucexg  4617  ordsucelsuc  4629  onzsl  4653  opelvvg  4750  opeliunxp2  4840  ideqg  4851  elrnmptg  4945  imasng  5051  elimasni  5056  iniseg  5060  elxp5  5177  dmmptg  5186  iota2  5261  fnmpt  5386  elfvex  5571  fvelimab  5594  fvmptdf  5627  fvmptdv2  5629  mpteqb  5630  fvmptt  5631  fvmptf  5632  fvopab6  5637  eloprabga  5950  ovmpt2s  5987  ov2gf  5988  ovmpt2dxf  5989  ovmpt2x  5992  ovmpt2ga  5993  ovmpt2df  5995  suppssfv  6090  suppssov1  6091  offval3  6107  releldm2  6186  fnmpt2  6208  mpt2exg  6212  brtpos2  6256  brrpssg  6295  sorpssi  6299  fvopab5  6305  pwuninel  6316  undefval  6317  riotasv2d  6365  riotasv2dOLD  6366  riotasv3d  6369  riotasv3dOLD  6370  tfr2b  6428  tz7.49  6473  oeordi  6601  oeeu  6617  relelec  6716  ecdmn0  6718  mapvalg  6798  pmvalg  6799  elpmg  6802  elixp2  6836  mptelixpg  6869  elixpsn  6871  2pwuninel  7032  pwfi  7167  fival  7182  elfi2  7184  dffi2  7192  elfiun  7199  wemappo  7280  wemapso  7282  wemapso2  7283  harval  7292  brwdom  7297  fowdom  7301  brwdom2  7303  brwdom3  7312  en2lp  7333  cantnfsuc  7387  cnfcomlem  7418  rankvalb  7485  pwwf  7495  rankwflem  7503  rankr1g  7520  r1pw  7533  r1pwOLD  7534  r1rankid  7547  cardval3  7601  pm54.43lem  7648  dfac8alem  7672  ac5num  7679  isacn  7687  numacn  7692  acndom  7694  cardinfima  7740  unialeph  7744  cdaval  7812  cflm  7892  isfin3  7938  isf32lem2  7996  isfin1-2  8027  itunifval  8058  numth3  8113  ttukeylem1  8152  ttukeylem3  8154  cardidg  8186  ondomon  8201  canth4  8285  canthnumlem  8286  canthwelem  8288  elwina  8324  elina  8325  wunex3  8379  wuncval  8380  grothpw  8464  tskmval  8477  eltskm  8481  recmulnq  8604  elnp  8627  elnpi  8628  npomex  8636  lbinfm  9723  elfzp12  10877  seqp1  11077  seqf1olem2  11102  hashinf  11358  hashxrcl  11367  hashbclem  11406  iswrd  11431  ccatfval  11444  swrdval  11466  splval  11482  splcl  11483  cats1un  11492  revval  11494  limsupcl  11963  limsupval  11964  clim  11984  rlim  11985  fsumrlim  12285  hashbcval  13065  isstruct2  13173  strfvnd  13179  setsvalg  13187  setscom  13192  strfv2d  13194  setsid  13203  ressval  13211  ressinbas  13220  restval  13347  prdsval  13371  prdssca  13372  pwsval  13401  imasval  13430  divsval  13460  xpsfrnel  13481  xpsfrnel2  13483  xpsval  13490  ismre  13508  oppcval  13632  brssc  13707  rescval  13720  issubc  13728  isfunc  13754  cofuval  13772  resfval  13782  funcres2c  13791  homadm  13888  homacd  13889  setcval  13925  catcval  13944  xpcval  13967  prfval  13989  curfval  14013  uncfval  14024  pltfval  14109  pospo  14123  lubfval  14128  glbfval  14133  joinfval  14137  meetfval  14144  p0val  14163  p1val  14164  pospropd  14254  oduclatb  14264  ipoval  14273  ipodrsima  14284  spwval2  14349  prdsmndd  14421  prds0g  14422  pws0g  14424  gsumvalx  14467  frmdval  14489  vrmdfval  14494  prdsgrpd  14620  prdsinvgd  14621  eqgfval  14681  eqgval  14682  gaid  14769  symgval  14787  elsymgbas  14790  cntzfval  14812  gexval  14905  sylow2a  14946  lsmfval  14965  pj1fval  15019  frgpval  15083  vrgpfval  15091  prdscmnd  15169  dmdprd  15252  dprdw  15261  pws1  15415  pwsmgp  15417  dvdsr  15444  isunit  15455  isirred  15497  issrng  15631  lssset  15707  prdslmodd  15742  lspfval  15746  islbs  15845  sraval  15945  psrval  16126  mvrfval  16181  ltbval  16229  opsrval  16232  coe1fval  16302  zlmval  16486  ocvfval  16582  cssval  16598  thlval  16611  eltopspOLD  16672  istpsOLD  16674  basdif0  16707  tgval  16709  eltg  16711  eltg2  16712  islp  16888  ordtval  16935  dis2ndc  17202  txval  17275  qtopval  17402  elmptrab2  17539  isfbas  17540  isfildlem  17568  snfil  17575  cfinfil  17604  csdfil  17605  supfil  17606  numufl  17626  fin1aufil  17643  fmval  17654  fmf  17656  isfcls  17720  alexsublem  17754  alexsub  17755  alexsubb  17756  tsmsfbas  17826  tsmsval2  17828  ismet  17904  isxmet  17905  prdsdsf  17947  prdsxmet  17949  comet  18075  tngval  18171  elpi1  18559  itgfsum  19197  evlsrhm  19421  evlssca  19422  evlsvar  19423  q1peqb  19556  ig1pval  19574  taylfval  19754  ulmval  19775  mtest  19797  avril1  20852  gidval  20896  elghomlem2  21045  isrngo  21061  isdivrngo  21114  isvc  21153  0vfval  21178  elunop  22468  ballotlemelo  23062  ballotlemsv  23084  rabexgfGS  23187  fmptpr  23229  abfmpunirn  23231  rabfmpunirn  23232  fnmptf  23242  funcnvmptOLD  23249  funcnvmpt  23250  disjdifprg  23367  disjdifprg2  23368  esumc  23445  esumpcvgval  23461  ofcfval  23474  ofcfval3  23478  issiga  23487  baselsiga  23491  sigasspw  23492  issgon  23499  isrnsigau  23503  sigagenval  23516  cldssbrsiga  23533  sxval  23536  ismeas  23545  cnmbfm  23583  mbfmcnt  23588  itgmcntTMP  23603  isibfm  23608  indv  23611  cndprobval  23651  orvcval  23673  vdgrfval  23904  relexpsucr  24041  eldm3  24190  elno  24371  nobndlem8  24424  nobndup  24425  nobnddown  24426  elfix2  24515  elsingles  24528  fvimage  24541  funpartlem  24552  elaltxp  24581  brcolinear2  24753  ellines  24847  limsucncmpi  24956  findabrcl  24965  alexeqd  25065  elo  25144  snelpwg  25194  sndw2  25204  ab2rexexg  25225  fprg  25236  ispr1  25259  isprj1  25266  iscst1  25277  cur1val  25301  domrancur1b  25303  isorhom  25314  isoriso  25315  oriso  25317  nfwval  25348  gepsup  25353  seinf  25354  ubos  25359  mxlelt  25367  mnlelt2  25369  fprod1i  25425  osneisi  25634  trdom  25716  supnufb  25733  issrc  25970  propsrc  25971  valtar  25986  trclval  25997  prismorcsetlemb  26016  grphidmor  26055  morexcmp  26070  cmppar3  26077  isword  26086  isnword  26089  isKleene  26091  selsubf3g  26095  lemindclsbu  26098  isconc1  26109  isconc2  26110  isconc3  26111  lineval5a  26191  lineval6a  26192  sgplpte21c  26238  sgplpte21d  26239  topfneec  26394  topfneec2  26395  islocfin  26399  neibastop1  26411  fnejoin2  26421  opelopab3  26476  elrfi  26872  nacsfix  26890  mapfzcons2  26899  mzpcl34  26912  sbc2rexg  26968  sbc4rexg  26969  setindtrs  27221  wepwso  27242  inisegn0  27243  dsmmval  27303  dsmmbase  27304  frlmval  27319  uvcfval  27336  elfilspd  27358  islinds  27382  hbtlem1  27430  hbtlem7  27432  rgspnval  27476  pmtrfval  27496  symggen  27514  mamufval  27546  matval  27568  mendval  27594  addrval  27774  subrval  27775  mulvval  27776  refsum2cnlem1  27811  dvcosre  27844  itgsinexplem1  27851  stoweidlem26  27878  stoweidlem28  27880  stoweidlem35  27887  stoweidlem55  27907  stoweidlem57  27909  stirlinglem14  27939  afvprc  28112  isuvtx  28301  wlks  28328  iswlkon  28332  trls  28335  trlon  28339  istrlon  28340  pths  28352  spths  28353  pthon  28361  crcts  28367  cycls  28368  bnj1463  29401  lshpset  29790  lsatset  29802  lcvfbr  29832  lflset  29871  lkrfval  29899  lkrval2  29902  islshpkrN  29932  ldualset  29937  cmtfvalN  30022  cvrfval  30080  pats  30097  llnset  30316  lplnset  30340  lvolset  30383  lineset  30549  pointsetN  30552  psubspset  30555  pmapfval  30567  paddfval  30608  pclfvalN  30700  polfvalN  30715  psubclsetN  30747  watfvalN  30803  lhpset  30806  lautset  30893  pautsetN  30909  ldilfset  30919  ltrnfset  30928  dilfsetN  30963  trnfsetN  30966  trlfset  30971  tgrpfset  31555  tendofset  31569  erngfset  31610  erngfset-rN  31618  dvafset  31815  diaffval  31842  dvhfset  31892  docaffvalN  31933  djaffvalN  31945  dibffval  31952  dicffval  31986  dihffval  32042  dochffval  32161  djhffval  32208  lpolsetN  32294  lcdfval  32400  mapdffval  32438  hvmapffval  32570  hdmap1ffval  32608  hdmapffval  32641  hgmapffval  32700  hlhilset  32749
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-11 1727  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1532  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-v 2803
  Copyright terms: Public domain W3C validator