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

Theorem elex 2797
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
StepHypRef Expression
1 exsimpl 1584 . 2  |-  ( E. x ( x  =  A  /\  x  e.  B )  ->  E. x  x  =  A )
2 df-clel 2280 . 2  |-  ( A  e.  B  <->  E. x
( x  =  A  /\  x  e.  B
) )
3 isset 2793 . 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 6    /\ wa 360   E.wex 1533    = wceq 1628    e. wcel 1688   _Vcvv 2789
This theorem is referenced by:  elexi  2798  elisset  2799  vtoclgft  2835  vtoclgf  2843  vtocl2gf  2846  vtocl3gf  2847  spcimgft  2860  elab4g  2919  elrabf  2923  mob  2948  sbcex  3001  sbcieg  3024  sbcrext  3065  sbcabel  3069  csbexg  3092  csbcomg  3105  csbvarg  3109  csbiebt  3118  csbnestgf  3130  csbidmg  3136  sbcco3g  3137  csbco3g  3139  eldif  3163  ssv  3199  elun  3317  elin  3359  snidb  3667  ifpr  3682  dfopg  3795  eluni  3831  eliun  3910  nvel  4154  class2seteq  4178  axpweq  4186  elopab  4271  epelg  4305  elon2  4402  ordsssuc2  4480  unexg  4520  reusv2lem4  4537  reuhypd  4560  elpwun  4566  ordeleqon  4579  ssonprc  4582  onintrab  4591  sucexg  4600  ordsucelsuc  4612  onzsl  4636  opelvvg  4733  opeliunxp2  4823  ideqg  4834  elrnmptg  4928  imasng  5034  elimasni  5039  iniseg  5043  elxp5  5159  dmmptg  5168  fnmpt  5335  elfvex  5516  fvelimab  5539  fvmptdf  5572  fvmptdv2  5574  mpteqb  5575  fvmptt  5576  fvmptf  5577  fvopab6  5582  eloprabga  5895  ovmpt2s  5932  ov2gf  5933  ovmpt2dxf  5934  ovmpt2x  5937  ovmpt2ga  5938  ovmpt2df  5940  suppssfv  6035  suppssov1  6036  offval3  6052  releldm2  6131  fnmpt2  6153  mpt2exg  6157  brtpos2  6201  brrpssg  6240  sorpssi  6244  iota2  6278  fvopab5  6282  pwuninel  6295  undefval  6296  riotasv2d  6344  riotasv2dOLD  6345  riotasv3d  6348  riotasv3dOLD  6349  tfr2b  6407  tz7.49  6452  oeordi  6580  oeeu  6596  relelec  6695  ecdmn0  6697  mapvalg  6777  pmvalg  6778  elpmg  6781  elixp2  6815  mptelixpg  6848  elixpsn  6850  2pwuninel  7011  pwfi  7146  fival  7161  elfi2  7163  dffi2  7171  elfiun  7178  wemappo  7259  wemapso  7261  wemapso2  7262  harval  7271  brwdom  7276  fowdom  7280  brwdom2  7282  brwdom3  7291  en2lp  7312  cantnfsuc  7366  cnfcomlem  7397  rankvalb  7464  pwwf  7474  rankwflem  7482  rankr1g  7499  r1pw  7512  r1pwOLD  7513  r1rankid  7526  cardval3  7580  pm54.43lem  7627  dfac8alem  7651  ac5num  7658  isacn  7666  numacn  7671  acndom  7673  cardinfima  7719  unialeph  7723  cdaval  7791  cflm  7871  isfin3  7917  isf32lem2  7975  isfin1-2  8006  itunifval  8037  numth3  8092  ttukeylem1  8131  ttukeylem3  8133  cardidg  8165  ondomon  8180  canth4  8264  canthnumlem  8265  canthwelem  8267  elwina  8303  elina  8304  wunexALT  8358  wuncval  8359  grothpw  8443  tskmval  8456  eltskm  8460  recmulnq  8583  elnp  8606  elnpi  8607  npomex  8615  lbinfm  9702  elfzp12  10855  seqp1  11055  seqf1olem2  11080  hashinf  11336  hashxrcl  11345  hashbclem  11384  iswrd  11409  ccatfval  11422  swrdval  11444  splval  11460  splcl  11461  cats1un  11470  revval  11472  limsupcl  11941  limsupval  11942  clim  11962  rlim  11963  fsumrlim  12263  hashbcval  13043  isstruct2  13151  strfvnd  13157  setsvalg  13165  setscom  13170  strfv2d  13172  setsid  13181  ressval  13189  ressinbas  13198  restval  13325  prdsval  13349  prdssca  13350  pwsval  13379  imasval  13408  divsval  13438  xpsfrnel  13459  xpsfrnel2  13461  xpsval  13468  ismre  13486  oppcval  13610  brssc  13685  rescval  13698  issubc  13706  isfunc  13732  cofuval  13750  resfval  13760  funcres2c  13769  homadm  13866  homacd  13867  setcval  13903  catcval  13922  xpcval  13945  prfval  13967  curfval  13991  uncfval  14002  pltfval  14087  pospo  14101  lubfval  14106  glbfval  14111  joinfval  14115  meetfval  14122  p0val  14141  p1val  14142  pospropd  14232  oduclatb  14242  ipoval  14251  ipodrsima  14262  spwval2  14327  prdsmndd  14399  prds0g  14400  pws0g  14402  gsumvalx  14445  frmdval  14467  vrmdfval  14472  prdsgrpd  14598  prdsinvgd  14599  eqgfval  14659  eqgval  14660  gaid  14747  symgval  14765  elsymgbas  14768  cntzfval  14790  gexval  14883  sylow2a  14924  lsmfval  14943  pj1fval  14997  frgpval  15061  vrgpfval  15069  prdscmnd  15147  dmdprd  15230  dprdw  15239  pws1  15393  pwsmgp  15395  dvdsr  15422  isunit  15433  isirred  15475  issrng  15609  lssset  15685  prdslmodd  15720  lspfval  15724  islbs  15823  sraval  15923  psrval  16104  mvrfval  16159  ltbval  16207  opsrval  16210  coe1fval  16280  zlmval  16464  ocvfval  16560  cssval  16576  thlval  16589  eltopspOLD  16650  istpsOLD  16652  basdif0  16685  tgval  16687  eltg  16689  eltg2  16690  islp  16866  ordtval  16913  dis2ndc  17180  txval  17253  qtopval  17380  elmptrab2  17517  isfbas  17518  isfildlem  17546  snfil  17553  cfinfil  17582  csdfil  17583  supfil  17584  numufl  17604  fin1aufil  17621  fmval  17632  fmf  17634  isfcls  17698  alexsublem  17732  alexsub  17733  alexsubb  17734  tsmsfbas  17804  tsmsval2  17806  ismet  17882  isxmet  17883  prdsdsf  17925  prdsxmet  17927  comet  18053  tngval  18149  elpi1  18537  itgfsum  19175  evlsrhm  19399  evlssca  19400  evlsvar  19401  q1peqb  19534  ig1pval  19552  taylfval  19732  ulmval  19753  mtest  19775  avril1  20828  gidval  20872  elghomlem2  21021  isrngo  21037  isdivrngo  21090  isvc  21129  0vfval  21154  elunop  22444  ballotlemelo  23039  ballotlemsv  23061  vdgrfval  23293  relexpsucr  23430  elno  23701  elfix2  23852  elsingles  23864  fvimage  23877  elaltxp  23916  brcolinear2  24088  ellines  24182  limsucncmpi  24291  findabrcl  24300  alexeqd  24360  elo  24439  snelpwg  24489  sndw2  24499  ab2rexexg  24521  fprg  24532  ispr1  24555  isprj1  24562  iscst1  24573  cur1val  24597  domrancur1b  24599  isorhom  24610  isoriso  24611  oriso  24613  nfwval  24644  gepsup  24649  seinf  24650  ubos  24655  mxlelt  24663  mnlelt2  24665  fprod1i  24721  osneisi  24930  trdom  25012  supnufb  25029  issrc  25266  propsrc  25267  valtar  25282  trclval  25293  prismorcsetlemb  25312  grphidmor  25351  morexcmp  25366  cmppar3  25373  isword  25382  isnword  25385  isKleene  25387  selsubf3g  25391  lemindclsbu  25394  isconc1  25405  isconc2  25406  isconc3  25407  lineval5a  25487  lineval6a  25488  sgplpte21c  25534  sgplpte21d  25535  topfneec  25690  topfneec2  25691  islocfin  25695  neibastop1  25707  fnejoin2  25717  opelopab3  25772  elrfi  26168  nacsfix  26186  mapfzcons2  26195  mzpcl34  26208  sbc2rexg  26264  sbc4rexg  26265  setindtrs  26517  wepwso  26538  inisegn0  26539  dsmmval  26599  dsmmbase  26600  frlmval  26615  uvcfval  26632  elfilspd  26654  islinds  26678  hbtlem1  26726  hbtlem7  26728  rgspnval  26772  pmtrfval  26792  symggen  26810  mamufval  26842  matval  26864  mendval  26890  addrval  27070  subrval  27071  mulvval  27072  refsum2cnlem1  27107  dvcosre  27140  itgsinexplem1  27147  stoweidlem26  27174  stoweidlem28  27176  stoweidlem35  27183  stoweidlem55  27203  stoweidlem57  27205  stirlinglem14  27235  afvprc  27384  bnj1463  28352  lshpset  28435  lsatset  28447  lcvfbr  28477  lflset  28516  lkrfval  28544  lkrval2  28547  islshpkrN  28577  ldualset  28582  cmtfvalN  28667  cvrfval  28725  pats  28742  llnset  28961  lplnset  28985  lvolset  29028  lineset  29194  pointsetN  29197  psubspset  29200  pmapfval  29212  paddfval  29253  pclfvalN  29345  polfvalN  29360  psubclsetN  29392  watfvalN  29448  lhpset  29451  lautset  29538  pautsetN  29554  ldilfset  29564  ltrnfset  29573  dilfsetN  29608  trnfsetN  29611  trlfset  29616  tgrpfset  30200  tendofset  30214  erngfset  30255  erngfset-rN  30263  dvafset  30460  diaffval  30487  dvhfset  30537  docaffvalN  30578  djaffvalN  30590  dibffval  30597  dicffval  30631  dihffval  30687  dochffval  30806  djhffval  30853  lpolsetN  30939  lcdfval  31045  mapdffval  31083  hvmapffval  31215  hdmap1ffval  31253  hdmapffval  31286  hgmapffval  31345  hlhilset  31394
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1538  ax-5 1549  ax-17 1608  ax-9 1641  ax-8 1648  ax-11 1719  ax-ext 2265
This theorem depends on definitions:  df-bi 179  df-an 362  df-ex 1534  df-sb 1636  df-clab 2271  df-cleq 2277  df-clel 2280  df-v 2791
  Copyright terms: Public domain W3C validator