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

Theorem elex 2796
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 1579 . 2  |-  ( E. x ( x  =  A  /\  x  e.  B )  ->  E. x  x  =  A )
2 df-clel 2279 . 2  |-  ( A  e.  B  <->  E. x
( x  =  A  /\  x  e.  B
) )
3 isset 2792 . 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 1528    = wceq 1623    e. wcel 1684   _Vcvv 2788
This theorem is referenced by:  elexi  2797  elisset  2798  vtoclgft  2834  vtoclgf  2842  vtocl2gf  2845  vtocl3gf  2846  spcimgft  2859  elab4g  2918  elrabf  2922  mob  2947  sbcex  3000  sbcieg  3023  sbcrext  3064  sbcabel  3068  csbexg  3091  csbcomg  3104  csbvarg  3108  csbiebt  3117  csbnestgf  3129  csbidmg  3135  sbcco3g  3136  csbco3g  3138  eldif  3162  ssv  3198  elun  3316  elin  3358  snidb  3666  ifpr  3681  dfopg  3794  eluni  3830  eliun  3909  nvel  4153  class2seteq  4179  axpweq  4187  elopab  4272  epelg  4306  elon2  4403  ordsssuc2  4481  unexg  4521  reusv2lem4  4538  reuhypd  4561  elpwun  4567  ordeleqon  4580  ssonprc  4583  onintrab  4592  sucexg  4601  ordsucelsuc  4613  onzsl  4637  opelvvg  4734  opeliunxp2  4824  ideqg  4835  elrnmptg  4929  imasng  5035  elimasni  5040  iniseg  5044  elxp5  5161  dmmptg  5170  iota2  5245  fnmpt  5370  elfvex  5555  fvelimab  5578  fvmptdf  5611  fvmptdv2  5613  mpteqb  5614  fvmptt  5615  fvmptf  5616  fvopab6  5621  eloprabga  5934  ovmpt2s  5971  ov2gf  5972  ovmpt2dxf  5973  ovmpt2x  5976  ovmpt2ga  5977  ovmpt2df  5979  suppssfv  6074  suppssov1  6075  offval3  6091  releldm2  6170  fnmpt2  6192  mpt2exg  6196  brtpos2  6240  brrpssg  6279  sorpssi  6283  fvopab5  6289  pwuninel  6300  undefval  6301  riotasv2d  6349  riotasv2dOLD  6350  riotasv3d  6353  riotasv3dOLD  6354  tfr2b  6412  tz7.49  6457  oeordi  6585  oeeu  6601  relelec  6700  ecdmn0  6702  mapvalg  6782  pmvalg  6783  elpmg  6786  elixp2  6820  mptelixpg  6853  elixpsn  6855  2pwuninel  7016  pwfi  7151  fival  7166  elfi2  7168  dffi2  7176  elfiun  7183  wemappo  7264  wemapso  7266  wemapso2  7267  harval  7276  brwdom  7281  fowdom  7285  brwdom2  7287  brwdom3  7296  en2lp  7317  cantnfsuc  7371  cnfcomlem  7402  rankvalb  7469  pwwf  7479  rankwflem  7487  rankr1g  7504  r1pw  7517  r1pwOLD  7518  r1rankid  7531  cardval3  7585  pm54.43lem  7632  dfac8alem  7656  ac5num  7663  isacn  7671  numacn  7676  acndom  7678  cardinfima  7724  unialeph  7728  cdaval  7796  cflm  7876  isfin3  7922  isf32lem2  7980  isfin1-2  8011  itunifval  8042  numth3  8097  ttukeylem1  8136  ttukeylem3  8138  cardidg  8170  ondomon  8185  canth4  8269  canthnumlem  8270  canthwelem  8272  elwina  8308  elina  8309  wunex3  8363  wuncval  8364  grothpw  8448  tskmval  8461  eltskm  8465  recmulnq  8588  elnp  8611  elnpi  8612  npomex  8620  lbinfm  9707  elfzp12  10861  seqp1  11061  seqf1olem2  11086  hashinf  11342  hashxrcl  11351  hashbclem  11390  iswrd  11415  ccatfval  11428  swrdval  11450  splval  11466  splcl  11467  cats1un  11476  revval  11478  limsupcl  11947  limsupval  11948  clim  11968  rlim  11969  fsumrlim  12269  hashbcval  13049  isstruct2  13157  strfvnd  13163  setsvalg  13171  setscom  13176  strfv2d  13178  setsid  13187  ressval  13195  ressinbas  13204  restval  13331  prdsval  13355  prdssca  13356  pwsval  13385  imasval  13414  divsval  13444  xpsfrnel  13465  xpsfrnel2  13467  xpsval  13474  ismre  13492  oppcval  13616  brssc  13691  rescval  13704  issubc  13712  isfunc  13738  cofuval  13756  resfval  13766  funcres2c  13775  homadm  13872  homacd  13873  setcval  13909  catcval  13928  xpcval  13951  prfval  13973  curfval  13997  uncfval  14008  pltfval  14093  pospo  14107  lubfval  14112  glbfval  14117  joinfval  14121  meetfval  14128  p0val  14147  p1val  14148  pospropd  14238  oduclatb  14248  ipoval  14257  ipodrsima  14268  spwval2  14333  prdsmndd  14405  prds0g  14406  pws0g  14408  gsumvalx  14451  frmdval  14473  vrmdfval  14478  prdsgrpd  14604  prdsinvgd  14605  eqgfval  14665  eqgval  14666  gaid  14753  symgval  14771  elsymgbas  14774  cntzfval  14796  gexval  14889  sylow2a  14930  lsmfval  14949  pj1fval  15003  frgpval  15067  vrgpfval  15075  prdscmnd  15153  dmdprd  15236  dprdw  15245  pws1  15399  pwsmgp  15401  dvdsr  15428  isunit  15439  isirred  15481  issrng  15615  lssset  15691  prdslmodd  15726  lspfval  15730  islbs  15829  sraval  15929  psrval  16110  mvrfval  16165  ltbval  16213  opsrval  16216  coe1fval  16286  zlmval  16470  ocvfval  16566  cssval  16582  thlval  16595  eltopspOLD  16656  istpsOLD  16658  basdif0  16691  tgval  16693  eltg  16695  eltg2  16696  islp  16872  ordtval  16919  dis2ndc  17186  txval  17259  qtopval  17386  elmptrab2  17523  isfbas  17524  isfildlem  17552  snfil  17559  cfinfil  17588  csdfil  17589  supfil  17590  numufl  17610  fin1aufil  17627  fmval  17638  fmf  17640  isfcls  17704  alexsublem  17738  alexsub  17739  alexsubb  17740  tsmsfbas  17810  tsmsval2  17812  ismet  17888  isxmet  17889  prdsdsf  17931  prdsxmet  17933  comet  18059  tngval  18155  elpi1  18543  itgfsum  19181  evlsrhm  19405  evlssca  19406  evlsvar  19407  q1peqb  19540  ig1pval  19558  taylfval  19738  ulmval  19759  mtest  19781  avril1  20836  gidval  20880  elghomlem2  21029  isrngo  21045  isdivrngo  21098  isvc  21137  0vfval  21162  elunop  22452  ballotlemelo  23046  ballotlemsv  23068  rabexgfGS  23171  fmptpr  23214  abfmpunirn  23216  rabfmpunirn  23217  fnmptf  23227  funcnvmptOLD  23234  funcnvmpt  23235  disjdifprg  23352  disjdifprg2  23353  esumc  23430  esumpcvgval  23446  ofcfval  23459  ofcfval3  23463  issiga  23472  baselsiga  23476  sigasspw  23477  issgon  23484  isrnsigau  23488  sigagenval  23501  cldssbrsiga  23518  sxval  23521  ismeas  23530  cnmbfm  23568  mbfmcnt  23573  itgmcntTMP  23588  isibfm  23593  indv  23596  cndprobval  23636  orvcval  23658  vdgrfval  23889  relexpsucr  24026  eldm3  24119  elno  24300  nobndlem8  24353  nobndup  24354  nobnddown  24355  elfix2  24444  elsingles  24457  fvimage  24470  elaltxp  24509  brcolinear2  24681  ellines  24775  limsucncmpi  24884  findabrcl  24893  alexeqd  24962  elo  25041  snelpwg  25091  sndw2  25101  ab2rexexg  25122  fprg  25133  ispr1  25156  isprj1  25163  iscst1  25174  cur1val  25198  domrancur1b  25200  isorhom  25211  isoriso  25212  oriso  25214  nfwval  25245  gepsup  25250  seinf  25251  ubos  25256  mxlelt  25264  mnlelt2  25266  fprod1i  25322  osneisi  25531  trdom  25613  supnufb  25630  issrc  25867  propsrc  25868  valtar  25883  trclval  25894  prismorcsetlemb  25913  grphidmor  25952  morexcmp  25967  cmppar3  25974  isword  25983  isnword  25986  isKleene  25988  selsubf3g  25992  lemindclsbu  25995  isconc1  26006  isconc2  26007  isconc3  26008  lineval5a  26088  lineval6a  26089  sgplpte21c  26135  sgplpte21d  26136  topfneec  26291  topfneec2  26292  islocfin  26296  neibastop1  26308  fnejoin2  26318  opelopab3  26373  elrfi  26769  nacsfix  26787  mapfzcons2  26796  mzpcl34  26809  sbc2rexg  26865  sbc4rexg  26866  setindtrs  27118  wepwso  27139  inisegn0  27140  dsmmval  27200  dsmmbase  27201  frlmval  27216  uvcfval  27233  elfilspd  27255  islinds  27279  hbtlem1  27327  hbtlem7  27329  rgspnval  27373  pmtrfval  27393  symggen  27411  mamufval  27443  matval  27465  mendval  27491  addrval  27671  subrval  27672  mulvval  27673  refsum2cnlem1  27708  dvcosre  27741  itgsinexplem1  27748  stoweidlem26  27775  stoweidlem28  27777  stoweidlem35  27784  stoweidlem55  27804  stoweidlem57  27806  stirlinglem14  27836  afvprc  28007  isuvtx  28160  bnj1463  29085  lshpset  29168  lsatset  29180  lcvfbr  29210  lflset  29249  lkrfval  29277  lkrval2  29280  islshpkrN  29310  ldualset  29315  cmtfvalN  29400  cvrfval  29458  pats  29475  llnset  29694  lplnset  29718  lvolset  29761  lineset  29927  pointsetN  29930  psubspset  29933  pmapfval  29945  paddfval  29986  pclfvalN  30078  polfvalN  30093  psubclsetN  30125  watfvalN  30181  lhpset  30184  lautset  30271  pautsetN  30287  ldilfset  30297  ltrnfset  30306  dilfsetN  30341  trnfsetN  30344  trlfset  30349  tgrpfset  30933  tendofset  30947  erngfset  30988  erngfset-rN  30996  dvafset  31193  diaffval  31220  dvhfset  31270  docaffvalN  31311  djaffvalN  31323  dibffval  31330  dicffval  31364  dihffval  31420  dochffval  31539  djhffval  31586  lpolsetN  31672  lcdfval  31778  mapdffval  31816  hvmapffval  31948  hdmap1ffval  31986  hdmapffval  32019  hgmapffval  32078  hlhilset  32127
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-11 1715  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1529  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-v 2790
  Copyright terms: Public domain W3C validator