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

Theorem elex 2748
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 1591 . 2  |-  ( E. x ( x  =  A  /\  x  e.  B )  ->  E. x  x  =  A )
2 df-clel 2252 . 2  |-  ( A  e.  B  <->  E. x
( x  =  A  /\  x  e.  B
) )
3 isset 2744 . 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 1537    = wceq 1619    e. wcel 1621   _Vcvv 2740
This theorem is referenced by:  elexi  2749  elisset  2750  vtoclgft  2785  vtoclgf  2793  vtocl2gf  2796  vtocl3gf  2797  cla4imgft  2810  elab4g  2869  elrabf  2873  mob  2898  sbcex  2944  sbcieg  2967  sbcrext  3008  sbcabel  3012  csbexg  3033  csbcomg  3046  csbvarg  3050  csbiebt  3059  csbnestgf  3071  csbidmg  3077  sbcco3g  3078  csbco3g  3080  eldif  3104  ssv  3140  elun  3258  elin  3300  snidb  3607  ifpr  3622  dfopg  3735  eluni  3771  eliun  3850  nvel  4093  class2seteq  4117  axpweq  4125  elopab  4209  epelg  4243  elon2  4340  ordsssuc2  4418  unexg  4458  reusv2lem4  4475  reuhypd  4498  elpwun  4504  ordeleqon  4517  ssonprc  4520  onintrab  4529  sucexg  4538  ordsucelsuc  4550  onzsl  4574  opelvvg  4687  opeliunxp2  4777  ideqg  4788  elrnmptg  4882  imasng  4988  elimasni  4993  iniseg  4997  elxp5  5113  dmmptg  5122  fnmpt  5273  elfvex  5454  fvelimab  5477  fvmptdf  5510  fvmptdv2  5512  mpteqb  5513  fvmptt  5514  fvmptf  5515  fvopab6  5520  eloprabga  5833  ovmpt2s  5870  ov2gf  5871  ovmpt2dxf  5872  ovmpt2x  5875  ovmpt2ga  5876  ovmpt2df  5878  suppssfv  5973  suppssov1  5974  offval3  5990  releldm2  6069  fnmpt2  6091  mpt2exg  6095  brtpos2  6139  brrpssg  6178  sorpssi  6182  iota2  6216  fvopab5  6220  pwuninel  6233  undefval  6234  riotasv2d  6282  riotasv2dOLD  6283  riotasv3d  6286  riotasv3dOLD  6287  tfr2b  6345  tz7.49  6390  oeordi  6518  oeeu  6534  relelec  6633  ecdmn0  6635  mapvalg  6715  pmvalg  6716  elpmg  6719  elixp2  6753  mptelixpg  6786  elixpsn  6788  2pwuninel  6949  pwfi  7084  fival  7099  elfi2  7101  dffi2  7109  elfiun  7116  wemappo  7197  wemapso  7199  wemapso2  7200  harval  7209  brwdom  7214  fowdom  7218  brwdom2  7220  brwdom3  7229  en2lp  7250  cantnfsuc  7304  cnfcomlem  7335  rankvalb  7402  pwwf  7412  rankwflem  7420  rankr1g  7437  r1pw  7450  r1pwOLD  7451  r1rankid  7464  cardval3  7518  pm54.43lem  7565  dfac8alem  7589  ac5num  7596  isacn  7604  numacn  7609  acndom  7611  cardinfima  7657  unialeph  7661  cdaval  7729  cflm  7809  isfin3  7855  isf32lem2  7913  isfin1-2  7944  itunifval  7975  numth3  8030  ttukeylem1  8069  ttukeylem3  8071  cardidg  8103  ondomon  8118  canth4  8202  canthnumlem  8203  canthwelem  8205  elwina  8241  elina  8242  wunexALT  8296  wuncval  8297  grothpw  8381  tskmval  8394  eltskm  8398  recmulnq  8521  elnp  8544  elnpi  8545  npomex  8553  lbinfm  9640  elfzp12  10792  seqp1  10992  seqf1olem2  11017  hashinf  11273  hashxrcl  11282  hashbclem  11320  iswrd  11345  ccatfval  11358  swrdval  11380  splval  11396  splcl  11397  cats1un  11406  revval  11408  limsupcl  11877  limsupval  11878  clim  11898  rlim  11899  fsumrlim  12199  hashbcval  12976  isstruct2  13084  strfvnd  13090  setsvalg  13098  setscom  13103  strfv2d  13105  setsid  13114  ressval  13122  ressinbas  13131  restval  13258  prdsval  13282  prdssca  13283  pwsval  13312  imasval  13341  divsval  13371  xpsfrnel  13392  xpsfrnel2  13394  xpsval  13401  ismre  13419  oppcval  13543  brssc  13618  rescval  13631  issubc  13639  isfunc  13665  cofuval  13683  resfval  13693  funcres2c  13702  homadm  13799  homacd  13800  setcval  13836  catcval  13855  xpcval  13878  prfval  13900  curfval  13924  uncfval  13935  pltfval  14020  pospo  14034  lubfval  14039  glbfval  14044  joinfval  14048  meetfval  14055  p0val  14074  p1val  14075  pospropd  14165  oduclatb  14175  ipoval  14184  ipodrsima  14195  spwval2  14260  prdsmndd  14332  prds0g  14333  pws0g  14335  gsumvalx  14378  frmdval  14400  vrmdfval  14405  prdsgrpd  14531  prdsinvgd  14532  eqgfval  14592  eqgval  14593  gaid  14680  symgval  14698  elsymgbas  14701  cntzfval  14723  gexval  14816  sylow2a  14857  lsmfval  14876  pj1fval  14930  frgpval  14994  vrgpfval  15002  prdscmnd  15080  dmdprd  15163  dprdw  15172  pws1  15326  pwsmgp  15328  dvdsr  15355  isunit  15366  isirred  15408  issrng  15542  lssset  15618  prdslmodd  15653  lspfval  15657  islbs  15756  sraval  15856  psrval  16037  mvrfval  16092  ltbval  16140  opsrval  16143  coe1fval  16213  zlmval  16397  ocvfval  16493  cssval  16509  thlval  16522  eltopspOLD  16583  istpsOLD  16585  basdif0  16618  tgval  16620  eltg  16622  eltg2  16623  islp  16799  ordtval  16846  dis2ndc  17113  txval  17186  qtopval  17313  elmptrab2  17450  isfbas  17451  isfildlem  17479  snfil  17486  cfinfil  17515  csdfil  17516  supfil  17517  numufl  17537  fin1aufil  17554  fmval  17565  fmf  17567  isfcls  17631  alexsublem  17665  alexsub  17666  alexsubb  17667  tsmsfbas  17737  tsmsval2  17739  ismet  17815  isxmet  17816  prdsdsf  17858  prdsxmet  17860  comet  17986  tngval  18082  elpi1  18470  itgfsum  19108  evlsrhm  19332  evlssca  19333  evlsvar  19334  q1peqb  19467  ig1pval  19485  taylfval  19665  ulmval  19686  mtest  19708  avril1  20761  gidval  20805  elghomlem2  20954  isrngo  20970  isdivrngo  21023  isvc  21062  0vfval  21087  elunop  22377  ballotlemelo  22972  ballotlemsv  22994  vdgrfval  23226  relexpsucr  23363  elno  23634  elfix2  23785  elsingles  23797  fvimage  23810  elaltxp  23849  brcolinear2  24021  ellines  24115  limsucncmpi  24224  findabrcl  24233  alexeqd  24293  elo  24372  snelpwg  24422  sndw2  24432  ab2rexexg  24454  fprg  24465  ispr1  24488  isprj1  24495  iscst1  24506  cur1val  24530  domrancur1b  24532  isorhom  24543  isoriso  24544  oriso  24546  nfwval  24577  gepsup  24582  seinf  24583  ubos  24588  mxlelt  24596  mnlelt2  24598  fprod1i  24654  osneisi  24863  trdom  24945  supnufb  24962  issrc  25199  propsrc  25200  valtar  25215  trclval  25226  prismorcsetlemb  25245  grphidmor  25284  morexcmp  25299  cmppar3  25306  isword  25315  isnword  25318  isKleene  25320  selsubf3g  25324  lemindclsbu  25327  isconc1  25338  isconc2  25339  isconc3  25340  lineval5a  25420  lineval6a  25421  sgplpte21c  25467  sgplpte21d  25468  topfneec  25623  topfneec2  25624  islocfin  25628  neibastop1  25640  fnejoin2  25650  opelopab3  25705  elrfi  26101  nacsfix  26119  mapfzcons2  26128  mzpcl34  26141  sbc2rexg  26197  sbc4rexg  26198  setindtrs  26450  wepwso  26471  inisegn0  26472  dsmmval  26532  dsmmbase  26533  frlmval  26548  uvcfval  26565  elfilspd  26587  islinds  26611  hbtlem1  26659  hbtlem7  26661  rgspnval  26705  pmtrfval  26725  symggen  26743  mamufval  26775  matval  26797  mendval  26823  addrval  27004  subrval  27005  mulvval  27006  refsum2cnlem1  27041  stoweidlem26  27075  stoweidlem28  27077  stoweidlem35  27084  stoweidlem55  27104  stoweidlem57  27106  bnj1463  28097  lshpset  28298  lsatset  28310  lcvfbr  28340  lflset  28379  lkrfval  28407  lkrval2  28410  islshpkrN  28440  ldualset  28445  cmtfvalN  28530  cvrfval  28588  pats  28605  llnset  28824  lplnset  28848  lvolset  28891  lineset  29057  pointsetN  29060  psubspset  29063  pmapfval  29075  paddfval  29116  pclfvalN  29208  polfvalN  29223  psubclsetN  29255  watfvalN  29311  lhpset  29314  lautset  29401  pautsetN  29417  ldilfset  29427  ltrnfset  29436  dilfsetN  29471  trnfsetN  29474  trlfset  29479  tgrpfset  30063  tendofset  30077  erngfset  30118  erngfset-rN  30126  dvafset  30323  diaffval  30350  dvhfset  30400  docaffvalN  30441  djaffvalN  30453  dibffval  30460  dicffval  30494  dihffval  30550  dochffval  30669  djhffval  30716  lpolsetN  30802  lcdfval  30908  mapdffval  30946  hvmapffval  31078  hdmap1ffval  31116  hdmapffval  31149  hgmapffval  31208  hlhilset  31257
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-gen 1536  ax-17 1628  ax-12o 1664  ax-9 1684  ax-4 1692  ax-ext 2237
This theorem depends on definitions:  df-bi 179  df-an 362  df-ex 1538  df-nf 1540  df-sb 1884  df-clab 2243  df-cleq 2249  df-clel 2252  df-v 2742
  Copyright terms: Public domain W3C validator