Theorem elisseti 2301

Description: If a class is a member of another class, it is a set.

Hypothesis

Ref	Expression
elisseti.1	|- A e. B

Assertion

Ref	Expression
elisseti	|- A e. _V

Proof of Theorem elisseti

Step	Hyp	Ref	Expression
1		elisseti.1	. 2 |- A e. B
2		elisset 2299	. 2 |- (A e. B -> A e. _V)
3	1, 2	ax-mp 7	1 |- A e. _V

Syntax hints:   e. wcel 1300  _Vcvv 2292

This theorem is referenced by:  onunisuci 3783  caoprmo 5003  tz7.44-2 5137  tz7.44-3 5138  oe0 5206  oev2 5207  oneo 5260  endisj 5496  pw2en 5505  pwen 5597  0sdom1dom 5618  pm54.43 5662  rankxplim3 5825  unxpdom2 5997  sucxpdom 5998  cfsuc 6063  uncdadom 6069  cdaun 6070  pm110.643 6072  cdaen 6073  cda1en 6076  cdacomen 6079  cdaassen 6080  mapcdaen 6082  nnacda 6088  nlt1pi 6185  indpi 6186  1qec 6220  mulidpq 6221  1lt2pq 6230  ltaddpq 6231  halfpq 6234  ltrpq 6237  1pr 6269  addclprlem1 6270  1idpr 6285  prlem934a 6289  prlem934b 6290  prlem936 6307  reclem3pr 6310  reclem4pr 6311  gt0srpr 6339  m1p1sr 6353  m1m1sr 6354  0lt1sr 6356  0idsr 6358  1idsr 6359  pn0sr 6362  recexsrlem 6364  addgt0sr 6365  sqgt0sr 6367  ssgt0sr 6369  mappsrpr 6370  ltpsrpr 6371  map2psrpr 6372  suppsr2 6375  suppsr3 6376  supsrlem1 6377  supsrlem2 6378  supsrlem3 6379  supsrlem5 6381  opelreal 6401  elreal 6402  eqresr 6407  mulresr 6409  axicn 6423  axmulass 6431  ax1ne0 6433  axi2m1 6438  axcnre 6439  pre-axmulgt0 6443  mnfxr 6662  elxr 6706  ssxrOLD 6715  1nn 7117  nn1suc 7122  xrsupss 7287  xrinfmss 7288  elnn0 7310  nn0ssz 7361  nn0ind-raph 7426  fzprval 7687  fztpval 7688  seq1lem1 7722  seq11lem 7728  expval 7813  facnn 8185  fac0 8186  bcval 8210  serz0 8313  serzcmp0 8315  binomlem1 8326  binomlem4 8329  binomlem6 8331  climuni 8359  climuz0i 8368  serzclim0 8369  climaddci 8392  iserzcmp0 8403  caucvg3 8428  ser1f0i 8430  ser1consti 8431  ser1clim0 8433  ser1cmp0i 8435  cvgcmpubi 8446  cvgcmp3cetlem1 8449  cvgcmp3cetlem2 8450  isumnn0nnai 8469  infcvgaux1i 8480  infcvglem2 8483  infcvglem3 8484  explecnv 8495  geolimilem 8497  efseq1ex 8568  dfef2i 8569  erelem2 8582  erelem4 8584  ele3lem 8588  ege2le3lem2 8591  ef0 8597  acdc2lem2 8758  acdc5lem2 8761  xpnnen 8768  ruclem6 8784  ruclem7 8785  ruclem8 8786  ruclem39 8817  infmap1 8842  infmap2 8850  dscmet 9196  fsumcnlem 9267  grpidvallem 9341  ipval2 9696  minveclem30 9919  minveclem31 9920  fora1 10406  zrdivrng 10418  hhph 10678  hlim0 10738  hlimcaui 10740  hlimunii 10742  hsn0elch 10753  elch0 10759  occllem6 10811  occllem7 10812  projlem17 10835  projlem31 10849  choc0 10923  shintcli 10926  shincli 10964  chincli 11016  h1deoi 11105  h1de2ctlem 11111  spansni 11113  osumlem5 11217  pjfni 11281  df0op2 11315  ho01i 11391  0cnfn 11541  0lnfn 11546  nmfn0 11548  nmop0h 11553  nmopun 11576  lnfnconi 11627  opsqrlem2 11712  opsqrlem3 11713  opsqrlem5 11715  pjnmopi 11719  atoml2i 11955  cdj3lem2 12007  bnj898 12815  bnj515 13256  bnj1015 13375  gcdval 13715  gcdf 13725  mulgcdlem2 13757  mulgcdlem4 13759  mulgcdlem5 13760  1nprm 13769  isprm2lem 13774  noxpsgn 13990  noxp1o 13991  noxp2o 13992  sltval2 13997  nofv 13998  sltsgn1 14002  sltsgn2 14003  sltintdifex 14004  axsltsolem1 14006  axbday 14012  axdenselem8 14026  axdense 14027  axfelem2 14032  axfelem6 14036  axfelem8 14038  axfelem9 14039  axfelem12 14042  fates 14292  dmoprabss6 14336  f1fi 14377  unpde2eg22 14407  fvsn2a 14451  fvsn2b 14452  repfuntw 14502  repcpwti 14503  prl 14512  dstr 14516  definc 14621  prodeq2 14661  fprodserz 14671  fprod1i 14673  fprodp1i 14674  fprod1slem 14676  fprodp1fi 14680  fprodp1slem 14681  seqzp2 14716  curgrpact 14735  eqindhome 14895  top2usne 14898  bintop 14901  stoig2b 14906  clindistop 14962  intopcon 14964  idtrgrp 14978  invtrgrp 14979  extopgrp 14980  cntrsetlem 14999  domleqt 15020  supexr 15043  supbrr 15048  fconst6 15700  sdc 15811  fdc 15812  seq1eq2 15817  fsumleisumi 15826  trirn 15834  oprpiece1res2 15881  txmet 15925  heiborlem3 15957  heiborlem5 15959  heiborlem7 15961  heiborlem8 15962  heiborlem18 15972  heiborlem20 15974  heiborlem25 15979  heiborlem26 15980  heiborlem29 15983  heiborlem40 15994  bfplem1 15998  bfplem2 15999  bfplem3 16000  bfplem8 16005  bfplem11 16008  bfp 16009  ismrer1 16024  pcocn 16076  pcopt 16084  pcorevlem 16086  stb2xpl 16742  stb3xpl 16743  divrngmclNEW 17164  invrcl 17171

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 1305  ax-12 1310  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-ext 1865

This theorem depends on definitions:  df-bi 164  df-an 242  df-ex 1327  df-sb 1536  df-clab 1872  df-cleq 1877  df-clel 1880  df-v 2294

Copyright terms: Public domain