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

Theorem elex 2735
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 2249 . 2  |-  ( A  e.  B  <->  E. x
( x  =  A  /\  x  e.  B
) )
3 isset 2731 . 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 2727
This theorem is referenced by:  elexi  2736  elisset  2737  vtoclgft  2772  vtoclgf  2780  vtocl2gf  2783  vtocl3gf  2784  cla4imgft  2797  elab4g  2855  elrabf  2859  mob  2884  sbcex  2930  sbcieg  2953  sbcrext  2994  sbcabel  2998  csbexg  3019  csbcomg  3032  csbvarg  3036  csbiebt  3045  csbnestgf  3057  csbidmg  3063  sbcco3g  3064  csbco3g  3066  eldif  3088  ssv  3119  elun  3226  elin  3266  snidb  3570  ifpr  3585  dfopg  3694  eluni  3730  eliun  3807  nvel  4050  class2seteq  4073  axpweq  4081  elopab  4165  epelg  4199  elon2  4296  ordsssuc2  4374  unexg  4412  reusv2lem4  4429  reuhypd  4452  elpwun  4458  ordeleqon  4471  ssonprc  4474  onintrab  4483  sucexg  4492  ordsucelsuc  4504  onzsl  4528  opelvvg  4641  opeliunxp2  4731  ideqg  4742  elrnmptg  4836  imasng  4942  elimasni  4947  iniseg  4951  elxp5  5067  dmmptg  5076  fnmpt  5227  elfvex  5408  fvelimab  5430  fvmptdf  5463  fvmptdv2  5465  mpteqb  5466  fvmptt  5467  fvmptf  5468  fvopab6  5473  eloprabga  5786  ovmpt2s  5823  ov2gf  5824  ovmpt2dxf  5825  ovmpt2x  5828  ovmpt2ga  5829  ovmpt2df  5831  suppssfv  5926  suppssov1  5927  offval3  5943  releldm2  6022  fnmpt2  6044  mpt2exg  6048  brtpos2  6092  brrpssg  6131  sorpssi  6135  iota2  6169  fvopab5  6173  pwuninel  6186  undefval  6187  riotasv2d  6235  riotasv2dOLD  6236  riotasv3d  6239  riotasv3dOLD  6240  tfr2b  6298  tz7.49  6343  oeordi  6471  oeeu  6487  relelec  6586  ecdmn0  6588  mapvalg  6668  pmvalg  6669  elpmg  6672  elixp2  6706  mptelixpg  6739  elixpsn  6741  2pwuninel  6901  pwfi  7035  fival  7050  elfi2  7052  dffi2  7060  elfiun  7067  wemappo  7148  wemapso  7150  wemapso2  7151  harval  7160  brwdom  7165  fowdom  7169  brwdom2  7171  brwdom3  7180  en2lp  7201  cantnfsuc  7255  cnfcomlem  7286  rankvalb  7353  pwwf  7363  rankwflem  7371  rankr1g  7388  r1pw  7401  r1pwOLD  7402  r1rankid  7415  cardval3  7469  pm54.43lem  7516  dfac8alem  7540  ac5num  7547  isacn  7555  numacn  7560  acndom  7562  cardinfima  7608  unialeph  7612  cdaval  7680  cflm  7760  isfin3  7806  isf32lem2  7864  isfin1-2  7895  itunifval  7926  numth3  7981  ttukeylem1  8020  ttukeylem3  8022  ondomon  8067  canth4  8149  canthnumlem  8150  canthwelem  8152  elwina  8188  elina  8189  wunexALT  8243  wuncval  8244  grothpw  8328  tskmval  8341  eltskm  8345  recmulnq  8468  elnp  8491  elnpi  8492  npomex  8500  lbinfm  9587  elfzp12  10739  seqp1  10939  seqf1olem2  10964  hashinf  11220  hashxrcl  11229  hashbclem  11267  iswrd  11292  ccatfval  11305  swrdval  11327  splval  11343  splcl  11344  cats1un  11353  revval  11355  limsupcl  11824  limsupval  11825  clim  11845  rlim  11846  fsumrlim  12146  hashbcval  12923  isstruct2  13031  strfvnd  13037  setsvalg  13045  setscom  13050  strfv2d  13052  setsid  13061  ressval  13069  ressinbas  13078  restval  13205  prdsval  13229  prdssca  13230  pwsval  13259  imasval  13288  divsval  13318  xpsfrnel  13339  xpsfrnel2  13341  xpsval  13348  ismre  13364  oppcval  13460  brssc  13535  rescval  13548  issubc  13556  isfunc  13582  cofuval  13600  resfval  13610  funcres2c  13619  homadm  13716  homacd  13717  setcval  13753  catcval  13772  xpcval  13795  prfval  13817  curfval  13841  uncfval  13852  pltfval  13937  pospo  13951  lubfval  13956  glbfval  13961  joinfval  13965  meetfval  13972  p0val  13991  p1val  13992  pospropd  14082  oduclatb  14092  ipoval  14101  ipodrsima  14112  spwval2  14168  prdsmndd  14240  prds0g  14241  pws0g  14243  gsumvalx  14286  frmdval  14308  vrmdfval  14313  prdsgrpd  14439  prdsinvgd  14440  eqgfval  14500  eqgval  14501  gaid  14588  symgval  14606  elsymgbas  14609  cntzfval  14631  gexval  14724  sylow2a  14765  lsmfval  14784  pj1fval  14838  frgpval  14902  vrgpfval  14910  prdscmnd  14988  dmdprd  15071  dprdw  15080  pws1  15234  pwsmgp  15236  dvdsr  15263  isunit  15274  isirred  15316  issrng  15450  lssset  15526  prdslmodd  15561  lspfval  15565  islbs  15664  sraval  15761  psrval  15942  mvrfval  15997  ltbval  16045  opsrval  16048  coe1fval  16118  zlmval  16302  ocvfval  16398  cssval  16414  thlval  16427  eltopspOLD  16488  istpsOLD  16490  basdif0  16523  tgval  16525  eltg  16527  eltg2  16528  islp  16704  ordtval  16751  dis2ndc  17018  txval  17091  qtopval  17218  elmptrab2  17355  isfbas  17356  isfildlem  17384  snfil  17391  cfinfil  17420  csdfil  17421  supfil  17422  numufl  17442  fin1aufil  17459  fmval  17470  fmf  17472  isfcls  17536  alexsublem  17570  alexsub  17571  alexsubb  17572  tsmsfbas  17642  tsmsval2  17644  ismet  17720  isxmet  17721  prdsdsf  17763  prdsxmet  17765  comet  17891  tngval  17987  elpi1  18375  itgfsum  19013  evlsrhm  19237  evlssca  19238  evlsvar  19239  q1peqb  19372  ig1pval  19390  taylfval  19570  ulmval  19591  mtest  19613  avril1  20666  gidval  20710  elghomlem2  20859  isrngo  20875  isdivrngo  20928  isvc  20967  0vfval  20992  elunop  22282  vdgrfval  23060  relexpsucr  23197  elno  23468  elfix2  23619  elsingles  23631  fvimage  23644  elaltxp  23683  brcolinear2  23855  ellines  23949  limsucncmpi  24058  findabrcl  24067  alexeqd  24127  elo  24206  snelpwg  24256  sndw2  24266  ab2rexexg  24288  fprg  24299  ispr1  24322  isprj1  24329  iscst1  24340  cur1val  24364  domrancur1b  24366  isorhom  24377  isoriso  24378  oriso  24380  nfwval  24411  gepsup  24416  seinf  24417  ubos  24422  mxlelt  24430  mnlelt2  24432  fprod1i  24488  osneisi  24697  trdom  24779  supnufb  24796  issrc  25033  propsrc  25034  valtar  25049  trclval  25060  prismorcsetlemb  25079  grphidmor  25118  morexcmp  25133  cmppar3  25140  isword  25149  isnword  25152  isKleene  25154  selsubf3g  25158  lemindclsbu  25161  isconc1  25172  isconc2  25173  isconc3  25174  lineval5a  25254  lineval6a  25255  sgplpte21c  25301  sgplpte21d  25302  topfneec  25457  topfneec2  25458  islocfin  25462  neibastop1  25474  fnejoin2  25484  opelopab3  25539  elrfi  25935  nacsfix  25953  mapfzcons2  25962  mzpcl34  25975  sbc2rexg  26031  sbc4rexg  26032  setindtrs  26284  wepwso  26305  inisegn0  26306  dsmmval  26366  dsmmbase  26367  frlmval  26382  uvcfval  26399  elfilspd  26421  islinds  26445  hbtlem1  26493  hbtlem7  26495  rgspnval  26539  pmtrfval  26559  symggen  26577  mamufval  26609  matval  26631  mendval  26657  addrval  26838  subrval  26839  mulvval  26840  bnj1463  27774  lshpset  27857  lsatset  27869  lcvfbr  27899  lflset  27938  lkrfval  27966  lkrval2  27969  islshpkrN  27999  ldualset  28004  cmtfvalN  28089  cvrfval  28147  pats  28164  llnset  28383  lplnset  28407  lvolset  28450  lineset  28616  pointsetN  28619  psubspset  28622  pmapfval  28634  paddfval  28675  pclfvalN  28767  polfvalN  28782  psubclsetN  28814  watfvalN  28870  lhpset  28873  lautset  28960  pautsetN  28976  ldilfset  28986  ltrnfset  28995  dilfsetN  29030  trnfsetN  29033  trlfset  29038  tgrpfset  29622  tendofset  29636  erngfset  29677  erngfset-rN  29685  dvafset  29882  diaffval  29909  dvhfset  29959  docaffvalN  30000  djaffvalN  30012  dibffval  30019  dicffval  30053  dihffval  30109  dochffval  30228  djhffval  30275  lpolsetN  30361  lcdfval  30467  mapdffval  30505  hvmapffval  30637  hdmap1ffval  30675  hdmapffval  30708  hgmapffval  30767  hlhilset  30816
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 2234
This theorem depends on definitions:  df-bi 179  df-an 362  df-ex 1538  df-nf 1540  df-sb 1883  df-clab 2240  df-cleq 2246  df-clel 2249  df-v 2729
  Copyright terms: Public domain W3C validator