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

Theorem elex 2966
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 1603 . 2  |-  ( E. x ( x  =  A  /\  x  e.  B )  ->  E. x  x  =  A )
2 df-clel 2434 . 2  |-  ( A  e.  B  <->  E. x
( x  =  A  /\  x  e.  B
) )
3 isset 2962 . 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 4    /\ wa 360   E.wex 1551    = wceq 1653    e. wcel 1726   _Vcvv 2958
This theorem is referenced by:  elexi  2967  elisset  2968  vtoclgft  3004  vtoclgf  3012  vtocl2gf  3015  vtocl3gf  3016  spcimgft  3029  elab4g  3088  elrabf  3093  mob  3118  sbcex  3172  sbcrext  3236  sbcabel  3240  csbexg  3263  csbcomg  3276  csbvarg  3280  csbiebt  3289  csbnestgf  3301  csbidmg  3306  sbcco3g  3307  csbco3g  3309  eldif  3332  ssv  3370  elun  3490  elin  3532  snidb  3842  ifpr  3858  dfopg  3984  eluni  4020  eliun  4099  nvel  4344  class2seteq  4370  axpweq  4378  elopab  4464  epelg  4497  elon2  4594  ordsssuc2  4672  unexg  4712  reusv2lem4  4729  reuhypd  4752  elpwun  4758  ordeleqon  4771  ssonprc  4774  onintrab  4783  sucexg  4792  ordsucelsuc  4804  onzsl  4828  opelvvg  4925  opeliunxp2  5015  ideqg  5026  elrnmptg  5122  imasng  5228  elimasni  5233  iniseg  5237  elxp5  5360  dmmptg  5369  iota2  5446  fnmpt  5573  elfvex  5760  fvelimab  5784  fvmptdf  5818  fvmptdv2  5820  mpteqb  5821  fvmptt  5822  fvmptf  5823  fvopab6  5828  fprg  5917  eloprabga  6162  ovmpt2s  6199  ov2gf  6200  ovmpt2dxf  6201  ovmpt2x  6204  ovmpt2ga  6205  ovmpt2df  6207  suppssfv  6303  suppssov1  6304  offval3  6320  releldm2  6399  fnmpt2  6421  mpt2exg  6425  brtpos2  6487  brrpssg  6526  sorpssi  6530  fvopab5  6536  pwuninel  6547  undefval  6548  riotasv2d  6596  riotasv2dOLD  6597  riotasv3d  6600  riotasv3dOLD  6601  tfr2b  6659  tz7.49  6704  oeordi  6832  oeeu  6848  relelec  6947  ecdmn0  6949  mapvalg  7030  pmvalg  7031  elpmg  7034  elixp2  7068  mptelixpg  7101  elixpsn  7103  2pwuninel  7264  pwfi  7404  fival  7419  elfi2  7421  dffi2  7430  elfiun  7437  wemappo  7520  wemapso  7522  wemapso2  7523  harval  7532  brwdom  7537  fowdom  7541  brwdom2  7543  brwdom3  7552  en2lp  7573  cantnfsuc  7627  cnfcomlem  7658  rankvalb  7725  pwwf  7735  rankwflem  7743  rankr1g  7760  r1pw  7773  r1pwOLD  7774  r1rankid  7787  cardval3  7841  pm54.43lem  7888  dfac8alem  7912  ac5num  7919  isacn  7927  numacn  7932  acndom  7934  cardinfima  7980  unialeph  7984  cdaval  8052  cflm  8132  isfin3  8178  isf32lem2  8236  isfin1-2  8267  itunifval  8298  numth3  8352  ttukeylem1  8391  ttukeylem3  8393  cardidg  8425  ondomon  8440  canth4  8524  canthnumlem  8525  canthwelem  8527  elwina  8563  elina  8564  wuncval  8619  grothpw  8703  tskmval  8716  eltskm  8720  recmulnq  8843  elnp  8866  elnpi  8867  npomex  8875  lbinfm  9963  elfzp12  11128  seqp1  11340  seqf1olem2  11365  hashinf  11625  hashnn0pnf  11628  hashxrcl  11642  hashbclem  11703  iswrd  11731  ccatfval  11744  swrdval  11766  splval  11782  splcl  11783  cats1un  11792  revval  11794  limsupcl  12269  limsupval  12270  clim  12290  rlim  12291  fsumrlim  12592  hashbcval  13372  isstruct2  13480  strfvnd  13486  setsvalg  13494  setscom  13499  strfv2d  13501  setsid  13510  ressval  13518  ressinbas  13527  restval  13656  prdsval  13680  prdssca  13681  pwsval  13710  imasval  13739  divsval  13769  xpsfrnel  13790  xpsfrnel2  13792  xpsval  13799  ismre  13817  oppcval  13941  brssc  14016  rescval  14029  issubc  14037  isfunc  14063  cofuval  14081  resfval  14091  funcres2c  14100  homadm  14197  homacd  14198  setcval  14234  catcval  14253  xpcval  14276  prfval  14298  curfval  14322  uncfval  14333  pltfval  14418  pospo  14432  lubfval  14437  glbfval  14442  joinfval  14446  meetfval  14453  p0val  14472  p1val  14473  pospropd  14563  oduclatb  14573  ipoval  14582  ipodrsima  14593  spwval2  14658  prdsmndd  14730  prds0g  14731  pws0g  14733  gsumvalx  14776  frmdval  14798  vrmdfval  14803  prdsgrpd  14929  prdsinvgd  14930  eqgfval  14990  eqgval  14991  gaid  15078  symgval  15096  elsymgbas  15099  cntzfval  15121  gexval  15214  sylow2a  15255  lsmfval  15274  pj1fval  15328  frgpval  15392  vrgpfval  15400  prdscmnd  15478  dmdprd  15561  dprdw  15570  pws1  15724  pwsmgp  15726  dvdsr  15753  isunit  15764  isirred  15806  issrng  15940  lssset  16012  prdslmodd  16047  lspfval  16051  islbs  16150  sraval  16250  psrval  16431  mvrfval  16486  ltbval  16534  opsrval  16537  coe1fval  16605  zlmval  16799  ocvfval  16895  cssval  16911  thlval  16924  eltopspOLD  16985  istpsOLD  16987  basdif0  17020  tgval  17022  eltg  17024  eltg2  17025  neipeltop  17195  islp  17206  ordtval  17255  dis2ndc  17525  txval  17598  qtopval  17729  elmptrab2  17862  isfbas  17863  isfildlem  17891  snfil  17898  cfinfil  17927  csdfil  17928  supfil  17929  numufl  17949  fin1aufil  17966  fmval  17977  fmf  17979  isfcls  18043  alexsub  18078  alexsubb  18079  tsmsfbas  18159  tsmsval2  18161  elutop  18265  isusp  18293  ispsmet  18337  ismet  18355  isxmet  18356  prdsdsf  18399  prdsxmet  18401  blfvalps  18415  metustelOLD  18583  metustel  18584  tngval  18682  elpi1  19072  itgfsum  19720  evlsrhm  19944  evlssca  19945  evlsvar  19946  q1peqb  20079  ig1pval  20097  taylfval  20277  ulmval  20298  mtest  20322  cusgrafilem1  21490  isuvtx  21499  wlks  21528  wlkon  21532  trls  21538  trlon  21542  2trllemA  21552  pths  21568  spths  21569  pthon  21577  spthon  21584  2wlklem1  21599  crcts  21611  cycls  21612  vdgrfval  21668  avril1  21759  gidval  21803  elghomlem2  21952  isrngo  21968  isdivrngo  22021  isvc  22062  0vfval  22087  elunop  23377  rabexgfGS  23989  disjdifprg  24019  disjdifprg2  24020  fmptpr  24064  abfmpunirn  24066  rabfmpunirn  24067  fnmptf  24076  funcnvmptOLD  24084  funcnvmpt  24085  inftmrel  24252  isinftm  24253  isarchi  24254  qqhval2  24368  rrhval  24381  xrhval  24386  indv  24412  esumc  24448  esumpcvgval  24470  ofcfval  24483  ofcfval3  24487  issiga  24496  baselsiga  24500  sigasspw  24501  issgon  24508  isrnsigau  24512  sigagenval  24525  cldssbrsiga  24543  sxval  24546  ismeas  24555  cnmbfm  24615  mbfmcnt  24620  sitgval  24649  sitmval  24663  orvcval  24717  orvcval4  24720  ballotlemsv  24769  relexpsucr  25132  eldm3  25387  opelco3  25405  elima4  25406  wsuclem  25578  elno  25603  nobndlem8  25656  nobndup  25657  nobnddown  25658  elfix2  25751  elsingles  25765  fvimage  25778  funpartlem  25789  elaltxp  25822  brcolinear2  25994  ellines  26088  limsucncmpi  26197  findabrcl  26206  topfneec  26373  topfneec2  26374  islocfin  26378  fnejoin2  26400  opelopab3  26420  elrfi  26750  nacsfix  26768  mapfzcons2  26777  sbc2rexg  26846  sbc4rexg  26847  setindtrs  27098  wepwso  27119  inisegn0  27120  dsmmval  27179  dsmmbase  27180  frlmval  27195  uvcfval  27212  elfilspd  27234  islinds  27258  hbtlem1  27306  hbtlem7  27308  rgspnval  27352  pmtrfval  27372  symggen  27390  mamufval  27422  matval  27444  mendval  27470  addrval  27649  subrval  27650  mulvval  27651  dvcosre  27719  itgsinexplem1  27726  stoweidlem26  27753  stoweidlem35  27762  stirlinglem14  27814  afvprc  27986  lswrd  28281  wwlk  28351  wwlkn  28352  is2wlkonot  28383  is2spthonot  28384  2wlksot  28387  2spthsot  28388  usgreghash2spot  28520  bnj1463  29486  lshpset  29838  lsatset  29850  lcvfbr  29880  lflset  29919  lkrfval  29947  lkrval2  29950  islshpkrN  29980  ldualset  29985  cmtfvalN  30070  cvrfval  30128  pats  30145  llnset  30364  lplnset  30388  lvolset  30431  lineset  30597  pointsetN  30600  psubspset  30603  pmapfval  30615  paddfval  30656  pclfvalN  30748  polfvalN  30763  psubclsetN  30795  watfvalN  30851  lhpset  30854  lautset  30941  pautsetN  30957  ldilfset  30967  ltrnfset  30976  dilfsetN  31011  trnfsetN  31014  trlfset  31019  tgrpfset  31603  tendofset  31617  erngfset  31658  erngfset-rN  31666  dvafset  31863  diaffval  31890  dvhfset  31940  docaffvalN  31981  djaffvalN  31993  dibffval  32000  dicffval  32034  dihffval  32090  dochffval  32209  djhffval  32256  lpolsetN  32342  lcdfval  32448  mapdffval  32486  hvmapffval  32618  hdmap1ffval  32656  hdmapffval  32689  hgmapffval  32748  hlhilset  32797
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-11 1762  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-an 362  df-ex 1552  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-v 2960
  Copyright terms: Public domain W3C validator