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

Theorem elex 2765
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 2761 . 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 2757
This theorem is referenced by:  elexi  2766  elisset  2767  vtoclgft  2802  vtoclgf  2810  vtocl2gf  2813  vtocl3gf  2814  cla4imgft  2827  elab4g  2886  elrabf  2890  mob  2915  sbcex  2961  sbcieg  2984  sbcrext  3025  sbcabel  3029  csbexg  3052  csbcomg  3065  csbvarg  3069  csbiebt  3078  csbnestgf  3090  csbidmg  3096  sbcco3g  3097  csbco3g  3099  eldif  3123  ssv  3159  elun  3277  elin  3319  snidb  3626  ifpr  3641  dfopg  3754  eluni  3790  eliun  3869  nvel  4113  class2seteq  4137  axpweq  4145  elopab  4230  epelg  4264  elon2  4361  ordsssuc2  4439  unexg  4479  reusv2lem4  4496  reuhypd  4519  elpwun  4525  ordeleqon  4538  ssonprc  4541  onintrab  4550  sucexg  4559  ordsucelsuc  4571  onzsl  4595  opelvvg  4708  opeliunxp2  4798  ideqg  4809  elrnmptg  4903  imasng  5009  elimasni  5014  iniseg  5018  elxp5  5134  dmmptg  5143  fnmpt  5294  elfvex  5475  fvelimab  5498  fvmptdf  5531  fvmptdv2  5533  mpteqb  5534  fvmptt  5535  fvmptf  5536  fvopab6  5541  eloprabga  5854  ovmpt2s  5891  ov2gf  5892  ovmpt2dxf  5893  ovmpt2x  5896  ovmpt2ga  5897  ovmpt2df  5899  suppssfv  5994  suppssov1  5995  offval3  6011  releldm2  6090  fnmpt2  6112  mpt2exg  6116  brtpos2  6160  brrpssg  6199  sorpssi  6203  iota2  6237  fvopab5  6241  pwuninel  6254  undefval  6255  riotasv2d  6303  riotasv2dOLD  6304  riotasv3d  6307  riotasv3dOLD  6308  tfr2b  6366  tz7.49  6411  oeordi  6539  oeeu  6555  relelec  6654  ecdmn0  6656  mapvalg  6736  pmvalg  6737  elpmg  6740  elixp2  6774  mptelixpg  6807  elixpsn  6809  2pwuninel  6970  pwfi  7105  fival  7120  elfi2  7122  dffi2  7130  elfiun  7137  wemappo  7218  wemapso  7220  wemapso2  7221  harval  7230  brwdom  7235  fowdom  7239  brwdom2  7241  brwdom3  7250  en2lp  7271  cantnfsuc  7325  cnfcomlem  7356  rankvalb  7423  pwwf  7433  rankwflem  7441  rankr1g  7458  r1pw  7471  r1pwOLD  7472  r1rankid  7485  cardval3  7539  pm54.43lem  7586  dfac8alem  7610  ac5num  7617  isacn  7625  numacn  7630  acndom  7632  cardinfima  7678  unialeph  7682  cdaval  7750  cflm  7830  isfin3  7876  isf32lem2  7934  isfin1-2  7965  itunifval  7996  numth3  8051  ttukeylem1  8090  ttukeylem3  8092  cardidg  8124  ondomon  8139  canth4  8223  canthnumlem  8224  canthwelem  8226  elwina  8262  elina  8263  wunexALT  8317  wuncval  8318  grothpw  8402  tskmval  8415  eltskm  8419  recmulnq  8542  elnp  8565  elnpi  8566  npomex  8574  lbinfm  9661  elfzp12  10813  seqp1  11013  seqf1olem2  11038  hashinf  11294  hashxrcl  11303  hashbclem  11341  iswrd  11366  ccatfval  11379  swrdval  11401  splval  11417  splcl  11418  cats1un  11427  revval  11429  limsupcl  11898  limsupval  11899  clim  11919  rlim  11920  fsumrlim  12220  hashbcval  12997  isstruct2  13105  strfvnd  13111  setsvalg  13119  setscom  13124  strfv2d  13126  setsid  13135  ressval  13143  ressinbas  13152  restval  13279  prdsval  13303  prdssca  13304  pwsval  13333  imasval  13362  divsval  13392  xpsfrnel  13413  xpsfrnel2  13415  xpsval  13422  ismre  13440  oppcval  13564  brssc  13639  rescval  13652  issubc  13660  isfunc  13686  cofuval  13704  resfval  13714  funcres2c  13723  homadm  13820  homacd  13821  setcval  13857  catcval  13876  xpcval  13899  prfval  13921  curfval  13945  uncfval  13956  pltfval  14041  pospo  14055  lubfval  14060  glbfval  14065  joinfval  14069  meetfval  14076  p0val  14095  p1val  14096  pospropd  14186  oduclatb  14196  ipoval  14205  ipodrsima  14216  spwval2  14281  prdsmndd  14353  prds0g  14354  pws0g  14356  gsumvalx  14399  frmdval  14421  vrmdfval  14426  prdsgrpd  14552  prdsinvgd  14553  eqgfval  14613  eqgval  14614  gaid  14701  symgval  14719  elsymgbas  14722  cntzfval  14744  gexval  14837  sylow2a  14878  lsmfval  14897  pj1fval  14951  frgpval  15015  vrgpfval  15023  prdscmnd  15101  dmdprd  15184  dprdw  15193  pws1  15347  pwsmgp  15349  dvdsr  15376  isunit  15387  isirred  15429  issrng  15563  lssset  15639  prdslmodd  15674  lspfval  15678  islbs  15777  sraval  15877  psrval  16058  mvrfval  16113  ltbval  16161  opsrval  16164  coe1fval  16234  zlmval  16418  ocvfval  16514  cssval  16530  thlval  16543  eltopspOLD  16604  istpsOLD  16606  basdif0  16639  tgval  16641  eltg  16643  eltg2  16644  islp  16820  ordtval  16867  dis2ndc  17134  txval  17207  qtopval  17334  elmptrab2  17471  isfbas  17472  isfildlem  17500  snfil  17507  cfinfil  17536  csdfil  17537  supfil  17538  numufl  17558  fin1aufil  17575  fmval  17586  fmf  17588  isfcls  17652  alexsublem  17686  alexsub  17687  alexsubb  17688  tsmsfbas  17758  tsmsval2  17760  ismet  17836  isxmet  17837  prdsdsf  17879  prdsxmet  17881  comet  18007  tngval  18103  elpi1  18491  itgfsum  19129  evlsrhm  19353  evlssca  19354  evlsvar  19355  q1peqb  19488  ig1pval  19506  taylfval  19686  ulmval  19707  mtest  19729  avril1  20782  gidval  20826  elghomlem2  20975  isrngo  20991  isdivrngo  21044  isvc  21083  0vfval  21108  elunop  22398  ballotlemelo  22993  ballotlemsv  23015  vdgrfval  23247  relexpsucr  23384  elno  23655  elfix2  23806  elsingles  23818  fvimage  23831  elaltxp  23870  brcolinear2  24042  ellines  24136  limsucncmpi  24245  findabrcl  24254  alexeqd  24314  elo  24393  snelpwg  24443  sndw2  24453  ab2rexexg  24475  fprg  24486  ispr1  24509  isprj1  24516  iscst1  24527  cur1val  24551  domrancur1b  24553  isorhom  24564  isoriso  24565  oriso  24567  nfwval  24598  gepsup  24603  seinf  24604  ubos  24609  mxlelt  24617  mnlelt2  24619  fprod1i  24675  osneisi  24884  trdom  24966  supnufb  24983  issrc  25220  propsrc  25221  valtar  25236  trclval  25247  prismorcsetlemb  25266  grphidmor  25305  morexcmp  25320  cmppar3  25327  isword  25336  isnword  25339  isKleene  25341  selsubf3g  25345  lemindclsbu  25348  isconc1  25359  isconc2  25360  isconc3  25361  lineval5a  25441  lineval6a  25442  sgplpte21c  25488  sgplpte21d  25489  topfneec  25644  topfneec2  25645  islocfin  25649  neibastop1  25661  fnejoin2  25671  opelopab3  25726  elrfi  26122  nacsfix  26140  mapfzcons2  26149  mzpcl34  26162  sbc2rexg  26218  sbc4rexg  26219  setindtrs  26471  wepwso  26492  inisegn0  26493  dsmmval  26553  dsmmbase  26554  frlmval  26569  uvcfval  26586  elfilspd  26608  islinds  26632  hbtlem1  26680  hbtlem7  26682  rgspnval  26726  pmtrfval  26746  symggen  26764  mamufval  26796  matval  26818  mendval  26844  addrval  27025  subrval  27026  mulvval  27027  refsum2cnlem1  27062  stoweidlem26  27096  stoweidlem28  27098  stoweidlem35  27105  stoweidlem55  27125  stoweidlem57  27127  bnj1463  28118  lshpset  28319  lsatset  28331  lcvfbr  28361  lflset  28400  lkrfval  28428  lkrval2  28431  islshpkrN  28461  ldualset  28466  cmtfvalN  28551  cvrfval  28609  pats  28626  llnset  28845  lplnset  28869  lvolset  28912  lineset  29078  pointsetN  29081  psubspset  29084  pmapfval  29096  paddfval  29137  pclfvalN  29229  polfvalN  29244  psubclsetN  29276  watfvalN  29332  lhpset  29335  lautset  29422  pautsetN  29438  ldilfset  29448  ltrnfset  29457  dilfsetN  29492  trnfsetN  29495  trlfset  29500  tgrpfset  30084  tendofset  30098  erngfset  30139  erngfset-rN  30147  dvafset  30344  diaffval  30371  dvhfset  30421  docaffvalN  30462  djaffvalN  30474  dibffval  30481  dicffval  30515  dihffval  30571  dochffval  30690  djhffval  30737  lpolsetN  30823  lcdfval  30929  mapdffval  30967  hvmapffval  31099  hdmap1ffval  31137  hdmapffval  31170  hgmapffval  31229  hlhilset  31278
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 2759
  Copyright terms: Public domain W3C validator