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

Theorem elex 2956
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 1602 . 2  |-  ( E. x ( x  =  A  /\  x  e.  B )  ->  E. x  x  =  A )
2 df-clel 2431 . 2  |-  ( A  e.  B  <->  E. x
( x  =  A  /\  x  e.  B
) )
3 isset 2952 . 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 1550    = wceq 1652    e. wcel 1725   _Vcvv 2948
This theorem is referenced by:  elexi  2957  elisset  2958  vtoclgft  2994  vtoclgf  3002  vtocl2gf  3005  vtocl3gf  3006  spcimgft  3019  elab4g  3078  elrabf  3083  mob  3108  sbcex  3162  sbcrext  3226  sbcabel  3230  csbexg  3253  csbcomg  3266  csbvarg  3270  csbiebt  3279  csbnestgf  3291  csbidmg  3296  sbcco3g  3297  csbco3g  3299  eldif  3322  ssv  3360  elun  3480  elin  3522  snidb  3832  ifpr  3848  dfopg  3974  eluni  4010  eliun  4089  nvel  4334  class2seteq  4360  axpweq  4368  elopab  4454  epelg  4487  elon2  4584  ordsssuc2  4662  unexg  4702  reusv2lem4  4719  reuhypd  4742  elpwun  4748  ordeleqon  4761  ssonprc  4764  onintrab  4773  sucexg  4782  ordsucelsuc  4794  onzsl  4818  opelvvg  4915  opeliunxp2  5005  ideqg  5016  elrnmptg  5112  imasng  5218  elimasni  5223  iniseg  5227  elxp5  5350  dmmptg  5359  iota2  5436  fnmpt  5563  elfvex  5750  fvelimab  5774  fvmptdf  5808  fvmptdv2  5810  mpteqb  5811  fvmptt  5812  fvmptf  5813  fvopab6  5818  fprg  5907  eloprabga  6152  ovmpt2s  6189  ov2gf  6190  ovmpt2dxf  6191  ovmpt2x  6194  ovmpt2ga  6195  ovmpt2df  6197  suppssfv  6293  suppssov1  6294  offval3  6310  releldm2  6389  fnmpt2  6411  mpt2exg  6415  brtpos2  6477  brrpssg  6516  sorpssi  6520  fvopab5  6526  pwuninel  6537  undefval  6538  riotasv2d  6586  riotasv2dOLD  6587  riotasv3d  6590  riotasv3dOLD  6591  tfr2b  6649  tz7.49  6694  oeordi  6822  oeeu  6838  relelec  6937  ecdmn0  6939  mapvalg  7020  pmvalg  7021  elpmg  7024  elixp2  7058  mptelixpg  7091  elixpsn  7093  2pwuninel  7254  pwfi  7394  fival  7409  elfi2  7411  dffi2  7420  elfiun  7427  wemappo  7508  wemapso  7510  wemapso2  7511  harval  7520  brwdom  7525  fowdom  7529  brwdom2  7531  brwdom3  7540  en2lp  7561  cantnfsuc  7615  cnfcomlem  7646  rankvalb  7713  pwwf  7723  rankwflem  7731  rankr1g  7748  r1pw  7761  r1pwOLD  7762  r1rankid  7775  cardval3  7829  pm54.43lem  7876  dfac8alem  7900  ac5num  7907  isacn  7915  numacn  7920  acndom  7922  cardinfima  7968  unialeph  7972  cdaval  8040  cflm  8120  isfin3  8166  isf32lem2  8224  isfin1-2  8255  itunifval  8286  numth3  8340  ttukeylem1  8379  ttukeylem3  8381  cardidg  8413  ondomon  8428  canth4  8512  canthnumlem  8513  canthwelem  8515  elwina  8551  elina  8552  wuncval  8607  grothpw  8691  tskmval  8704  eltskm  8708  recmulnq  8831  elnp  8854  elnpi  8855  npomex  8863  lbinfm  9951  elfzp12  11116  seqp1  11328  seqf1olem2  11353  hashinf  11613  hashnn0pnf  11616  hashxrcl  11630  hashbclem  11691  iswrd  11719  ccatfval  11732  swrdval  11754  splval  11770  splcl  11771  cats1un  11780  revval  11782  limsupcl  12257  limsupval  12258  clim  12278  rlim  12279  fsumrlim  12580  hashbcval  13360  isstruct2  13468  strfvnd  13474  setsvalg  13482  setscom  13487  strfv2d  13489  setsid  13498  ressval  13506  ressinbas  13515  restval  13644  prdsval  13668  prdssca  13669  pwsval  13698  imasval  13727  divsval  13757  xpsfrnel  13778  xpsfrnel2  13780  xpsval  13787  ismre  13805  oppcval  13929  brssc  14004  rescval  14017  issubc  14025  isfunc  14051  cofuval  14069  resfval  14079  funcres2c  14088  homadm  14185  homacd  14186  setcval  14222  catcval  14241  xpcval  14264  prfval  14286  curfval  14310  uncfval  14321  pltfval  14406  pospo  14420  lubfval  14425  glbfval  14430  joinfval  14434  meetfval  14441  p0val  14460  p1val  14461  pospropd  14551  oduclatb  14561  ipoval  14570  ipodrsima  14581  spwval2  14646  prdsmndd  14718  prds0g  14719  pws0g  14721  gsumvalx  14764  frmdval  14786  vrmdfval  14791  prdsgrpd  14917  prdsinvgd  14918  eqgfval  14978  eqgval  14979  gaid  15066  symgval  15084  elsymgbas  15087  cntzfval  15109  gexval  15202  sylow2a  15243  lsmfval  15262  pj1fval  15316  frgpval  15380  vrgpfval  15388  prdscmnd  15466  dmdprd  15549  dprdw  15558  pws1  15712  pwsmgp  15714  dvdsr  15741  isunit  15752  isirred  15794  issrng  15928  lssset  16000  prdslmodd  16035  lspfval  16039  islbs  16138  sraval  16238  psrval  16419  mvrfval  16474  ltbval  16522  opsrval  16525  coe1fval  16593  zlmval  16787  ocvfval  16883  cssval  16899  thlval  16912  eltopspOLD  16973  istpsOLD  16975  basdif0  17008  tgval  17010  eltg  17012  eltg2  17013  neipeltop  17183  islp  17194  ordtval  17243  dis2ndc  17513  txval  17586  qtopval  17717  elmptrab2  17850  isfbas  17851  isfildlem  17879  snfil  17886  cfinfil  17915  csdfil  17916  supfil  17917  numufl  17937  fin1aufil  17954  fmval  17965  fmf  17967  isfcls  18031  alexsub  18066  alexsubb  18067  tsmsfbas  18147  tsmsval2  18149  elutop  18253  isusp  18281  ispsmet  18325  ismet  18343  isxmet  18344  prdsdsf  18387  prdsxmet  18389  blfvalps  18403  metustelOLD  18571  metustel  18572  tngval  18670  elpi1  19060  itgfsum  19708  evlsrhm  19932  evlssca  19933  evlsvar  19934  q1peqb  20067  ig1pval  20085  taylfval  20265  ulmval  20286  mtest  20310  cusgrafilem1  21478  isuvtx  21487  wlks  21516  wlkon  21520  trls  21526  trlon  21530  2trllemA  21540  pths  21556  spths  21557  pthon  21565  spthon  21572  2wlklem1  21587  crcts  21599  cycls  21600  vdgrfval  21656  avril1  21747  gidval  21791  elghomlem2  21940  isrngo  21956  isdivrngo  22009  isvc  22050  0vfval  22075  elunop  23365  rabexgfGS  23977  disjdifprg  24007  disjdifprg2  24008  fmptpr  24052  abfmpunirn  24054  rabfmpunirn  24055  fnmptf  24064  funcnvmptOLD  24072  funcnvmpt  24073  inftmrel  24240  isinftm  24241  isarchi  24242  qqhval2  24356  rrhval  24369  xrhval  24374  indv  24400  esumc  24436  esumpcvgval  24458  ofcfval  24471  ofcfval3  24475  issiga  24484  baselsiga  24488  sigasspw  24489  issgon  24496  isrnsigau  24500  sigagenval  24513  cldssbrsiga  24531  sxval  24534  ismeas  24543  cnmbfm  24603  mbfmcnt  24608  sitgval  24637  sitmval  24651  orvcval  24705  orvcval4  24708  ballotlemsv  24757  relexpsucr  25120  eldm3  25375  opelco3  25391  elima4  25392  elno  25566  nobndlem8  25619  nobndup  25620  nobnddown  25621  elfix2  25714  elsingles  25728  fvimage  25741  funpartlem  25752  elaltxp  25785  brcolinear2  25957  ellines  26051  limsucncmpi  26160  findabrcl  26169  topfneec  26325  topfneec2  26326  islocfin  26330  fnejoin2  26352  opelopab3  26372  elrfi  26702  nacsfix  26720  mapfzcons2  26729  sbc2rexg  26798  sbc4rexg  26799  setindtrs  27050  wepwso  27071  inisegn0  27072  dsmmval  27132  dsmmbase  27133  frlmval  27148  uvcfval  27165  elfilspd  27187  islinds  27211  hbtlem1  27259  hbtlem7  27261  rgspnval  27305  pmtrfval  27325  symggen  27343  mamufval  27375  matval  27397  mendval  27423  addrval  27602  subrval  27603  mulvval  27604  dvcosre  27672  itgsinexplem1  27679  stoweidlem26  27706  stoweidlem35  27715  stirlinglem14  27767  afvprc  27939  lswrd  28189  is2wlkonot  28247  is2spthonot  28248  2wlksot  28251  2spthsot  28252  usgreghash2spot  28359  bnj1463  29325  lshpset  29677  lsatset  29689  lcvfbr  29719  lflset  29758  lkrfval  29786  lkrval2  29789  islshpkrN  29819  ldualset  29824  cmtfvalN  29909  cvrfval  29967  pats  29984  llnset  30203  lplnset  30227  lvolset  30270  lineset  30436  pointsetN  30439  psubspset  30442  pmapfval  30454  paddfval  30495  pclfvalN  30587  polfvalN  30602  psubclsetN  30634  watfvalN  30690  lhpset  30693  lautset  30780  pautsetN  30796  ldilfset  30806  ltrnfset  30815  dilfsetN  30850  trnfsetN  30853  trlfset  30858  tgrpfset  31442  tendofset  31456  erngfset  31497  erngfset-rN  31505  dvafset  31702  diaffval  31729  dvhfset  31779  docaffvalN  31820  djaffvalN  31832  dibffval  31839  dicffval  31873  dihffval  31929  dochffval  32048  djhffval  32095  lpolsetN  32181  lcdfval  32287  mapdffval  32325  hvmapffval  32457  hdmap1ffval  32495  hdmapffval  32528  hgmapffval  32587  hlhilset  32636
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-11 1761  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1551  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-v 2950
  Copyright terms: Public domain W3C validator