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

Theorem elex 2924
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 2400 . 2  |-  ( A  e.  B  <->  E. x
( x  =  A  /\  x  e.  B
) )
3 isset 2920 . 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 1721   _Vcvv 2916
This theorem is referenced by:  elexi  2925  elisset  2926  vtoclgft  2962  vtoclgf  2970  vtocl2gf  2973  vtocl3gf  2974  spcimgft  2987  elab4g  3046  elrabf  3051  mob  3076  sbcex  3130  sbcrext  3194  sbcabel  3198  csbexg  3221  csbcomg  3234  csbvarg  3238  csbiebt  3247  csbnestgf  3259  csbidmg  3264  sbcco3g  3265  csbco3g  3267  eldif  3290  ssv  3328  elun  3448  elin  3490  snidb  3800  ifpr  3816  dfopg  3942  eluni  3978  eliun  4057  nvel  4302  class2seteq  4328  axpweq  4336  elopab  4422  epelg  4455  elon2  4552  ordsssuc2  4629  unexg  4669  reusv2lem4  4686  reuhypd  4709  elpwun  4715  ordeleqon  4728  ssonprc  4731  onintrab  4740  sucexg  4749  ordsucelsuc  4761  onzsl  4785  opelvvg  4882  opeliunxp2  4972  ideqg  4983  elrnmptg  5079  imasng  5185  elimasni  5190  iniseg  5194  elxp5  5317  dmmptg  5326  iota2  5403  fnmpt  5530  elfvex  5717  fvelimab  5741  fvmptdf  5775  fvmptdv2  5777  mpteqb  5778  fvmptt  5779  fvmptf  5780  fvopab6  5785  fprg  5874  eloprabga  6119  ovmpt2s  6156  ov2gf  6157  ovmpt2dxf  6158  ovmpt2x  6161  ovmpt2ga  6162  ovmpt2df  6164  suppssfv  6260  suppssov1  6261  offval3  6277  releldm2  6356  fnmpt2  6378  mpt2exg  6382  brtpos2  6444  brrpssg  6483  sorpssi  6487  fvopab5  6493  pwuninel  6504  undefval  6505  riotasv2d  6553  riotasv2dOLD  6554  riotasv3d  6557  riotasv3dOLD  6558  tfr2b  6616  tz7.49  6661  oeordi  6789  oeeu  6805  relelec  6904  ecdmn0  6906  mapvalg  6987  pmvalg  6988  elpmg  6991  elixp2  7025  mptelixpg  7058  elixpsn  7060  2pwuninel  7221  pwfi  7360  fival  7375  elfi2  7377  dffi2  7386  elfiun  7393  wemappo  7474  wemapso  7476  wemapso2  7477  harval  7486  brwdom  7491  fowdom  7495  brwdom2  7497  brwdom3  7506  en2lp  7527  cantnfsuc  7581  cnfcomlem  7612  rankvalb  7679  pwwf  7689  rankwflem  7697  rankr1g  7714  r1pw  7727  r1pwOLD  7728  r1rankid  7741  cardval3  7795  pm54.43lem  7842  dfac8alem  7866  ac5num  7873  isacn  7881  numacn  7886  acndom  7888  cardinfima  7934  unialeph  7938  cdaval  8006  cflm  8086  isfin3  8132  isf32lem2  8190  isfin1-2  8221  itunifval  8252  numth3  8306  ttukeylem1  8345  ttukeylem3  8347  cardidg  8379  ondomon  8394  canth4  8478  canthnumlem  8479  canthwelem  8481  elwina  8517  elina  8518  wuncval  8573  grothpw  8657  tskmval  8670  eltskm  8674  recmulnq  8797  elnp  8820  elnpi  8821  npomex  8829  lbinfm  9917  elfzp12  11081  seqp1  11293  seqf1olem2  11318  hashinf  11578  hashnn0pnf  11581  hashxrcl  11595  hashbclem  11656  iswrd  11684  ccatfval  11697  swrdval  11719  splval  11735  splcl  11736  cats1un  11745  revval  11747  limsupcl  12222  limsupval  12223  clim  12243  rlim  12244  fsumrlim  12545  hashbcval  13325  isstruct2  13433  strfvnd  13439  setsvalg  13447  setscom  13452  strfv2d  13454  setsid  13463  ressval  13471  ressinbas  13480  restval  13609  prdsval  13633  prdssca  13634  pwsval  13663  imasval  13692  divsval  13722  xpsfrnel  13743  xpsfrnel2  13745  xpsval  13752  ismre  13770  oppcval  13894  brssc  13969  rescval  13982  issubc  13990  isfunc  14016  cofuval  14034  resfval  14044  funcres2c  14053  homadm  14150  homacd  14151  setcval  14187  catcval  14206  xpcval  14229  prfval  14251  curfval  14275  uncfval  14286  pltfval  14371  pospo  14385  lubfval  14390  glbfval  14395  joinfval  14399  meetfval  14406  p0val  14425  p1val  14426  pospropd  14516  oduclatb  14526  ipoval  14535  ipodrsima  14546  spwval2  14611  prdsmndd  14683  prds0g  14684  pws0g  14686  gsumvalx  14729  frmdval  14751  vrmdfval  14756  prdsgrpd  14882  prdsinvgd  14883  eqgfval  14943  eqgval  14944  gaid  15031  symgval  15049  elsymgbas  15052  cntzfval  15074  gexval  15167  sylow2a  15208  lsmfval  15227  pj1fval  15281  frgpval  15345  vrgpfval  15353  prdscmnd  15431  dmdprd  15514  dprdw  15523  pws1  15677  pwsmgp  15679  dvdsr  15706  isunit  15717  isirred  15759  issrng  15893  lssset  15965  prdslmodd  16000  lspfval  16004  islbs  16103  sraval  16203  psrval  16384  mvrfval  16439  ltbval  16487  opsrval  16490  coe1fval  16558  zlmval  16752  ocvfval  16848  cssval  16864  thlval  16877  eltopspOLD  16938  istpsOLD  16940  basdif0  16973  tgval  16975  eltg  16977  eltg2  16978  neipeltop  17148  islp  17159  ordtval  17207  dis2ndc  17476  txval  17549  qtopval  17680  elmptrab2  17813  isfbas  17814  isfildlem  17842  snfil  17849  cfinfil  17878  csdfil  17879  supfil  17880  numufl  17900  fin1aufil  17917  fmval  17928  fmf  17930  isfcls  17994  alexsub  18029  alexsubb  18030  tsmsfbas  18110  tsmsval2  18112  elutop  18216  isusp  18244  ispsmet  18288  ismet  18306  isxmet  18307  prdsdsf  18350  prdsxmet  18352  blfvalps  18366  metustelOLD  18534  metustel  18535  tngval  18633  elpi1  19023  itgfsum  19671  evlsrhm  19895  evlssca  19896  evlsvar  19897  q1peqb  20030  ig1pval  20048  taylfval  20228  ulmval  20249  mtest  20273  cusgrafilem1  21441  isuvtx  21450  wlks  21479  wlkon  21483  trls  21489  trlon  21493  2trllemA  21503  pths  21519  spths  21520  pthon  21528  spthon  21535  2wlklem1  21550  crcts  21562  cycls  21563  vdgrfval  21619  avril1  21710  gidval  21754  elghomlem2  21903  isrngo  21919  isdivrngo  21972  isvc  22013  0vfval  22038  elunop  23328  rabexgfGS  23940  disjdifprg  23970  disjdifprg2  23971  fmptpr  24015  abfmpunirn  24017  rabfmpunirn  24018  fnmptf  24027  funcnvmptOLD  24035  funcnvmpt  24036  inftmrel  24203  isinftm  24204  isarchi  24205  qqhval2  24319  rrhval  24332  xrhval  24337  indv  24363  esumc  24399  esumpcvgval  24421  ofcfval  24434  ofcfval3  24438  issiga  24447  baselsiga  24451  sigasspw  24452  issgon  24459  isrnsigau  24463  sigagenval  24476  cldssbrsiga  24494  sxval  24497  ismeas  24506  cnmbfm  24566  mbfmcnt  24571  sitgval  24600  sitmval  24614  orvcval  24668  orvcval4  24671  ballotlemsv  24720  relexpsucr  25083  eldm3  25333  elno  25514  nobndlem8  25567  nobndup  25568  nobnddown  25569  elfix2  25658  elsingles  25671  fvimage  25684  funpartlem  25695  elaltxp  25724  brcolinear2  25896  ellines  25990  limsucncmpi  26099  findabrcl  26108  topfneec  26261  topfneec2  26262  islocfin  26266  fnejoin2  26288  opelopab3  26308  elrfi  26638  nacsfix  26656  mapfzcons2  26665  sbc2rexg  26734  sbc4rexg  26735  setindtrs  26986  wepwso  27007  inisegn0  27008  dsmmval  27068  dsmmbase  27069  frlmval  27084  uvcfval  27101  elfilspd  27123  islinds  27147  hbtlem1  27195  hbtlem7  27197  rgspnval  27241  pmtrfval  27261  symggen  27279  mamufval  27311  matval  27333  mendval  27359  addrval  27538  subrval  27539  mulvval  27540  dvcosre  27608  itgsinexplem1  27615  stoweidlem26  27642  stoweidlem35  27651  stirlinglem14  27703  afvprc  27875  is2wlkonot  28060  is2spthonot  28061  2wlksot  28064  2spthsot  28065  usgreghash2spot  28172  bnj1463  29130  lshpset  29461  lsatset  29473  lcvfbr  29503  lflset  29542  lkrfval  29570  lkrval2  29573  islshpkrN  29603  ldualset  29608  cmtfvalN  29693  cvrfval  29751  pats  29768  llnset  29987  lplnset  30011  lvolset  30054  lineset  30220  pointsetN  30223  psubspset  30226  pmapfval  30238  paddfval  30279  pclfvalN  30371  polfvalN  30386  psubclsetN  30418  watfvalN  30474  lhpset  30477  lautset  30564  pautsetN  30580  ldilfset  30590  ltrnfset  30599  dilfsetN  30634  trnfsetN  30637  trlfset  30642  tgrpfset  31226  tendofset  31240  erngfset  31281  erngfset-rN  31289  dvafset  31486  diaffval  31513  dvhfset  31563  docaffvalN  31604  djaffvalN  31616  dibffval  31623  dicffval  31657  dihffval  31713  dochffval  31832  djhffval  31879  lpolsetN  31965  lcdfval  32071  mapdffval  32109  hvmapffval  32241  hdmap1ffval  32279  hdmapffval  32312  hgmapffval  32371  hlhilset  32420
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 1662  ax-8 1683  ax-11 1757  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1548  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-v 2918
  Copyright terms: Public domain W3C validator