Theorem elisseti 1864

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 1863	. 2 |- (A e. B -> A e. V)
3	1, 2	ax-mp 7	1 |- A e. V

Syntax hints:   e. wcel 994  Vcvv 1857

This theorem is referenced by:  onunisuci 3083  caoprmo 4131  tz7.44-2 4230  tz7.44-3 4231  oe0 4297  oev2 4298  oneo 4348  endisj 4578  pw2en 4587  pwen 4650  0sdom1dom 4671  pm54.43 4715  rankxplim3 4860  unxpdom2 4995  sucxpdom 4996  cfsuc 5065  uncdadom 5071  cdaun 5072  pm110.643 5074  cdaen 5075  cda1en 5078  cdacomen 5081  cdaassen 5082  mapcdaen 5084  nnacda 5090  nlt1pi 5187  indpi 5188  1qec 5222  mulidpq 5223  1lt2pq 5232  ltaddpq 5233  halfpq 5236  ltrpq 5239  1pr 5271  addclprlem1 5272  1idpr 5287  prlem934a 5291  prlem934b 5292  prlem936 5309  reclem3pr 5312  reclem4pr 5313  gt0srpr 5341  m1p1sr 5355  m1m1sr 5356  0lt1sr 5358  0idsr 5360  1idsr 5361  pn0sr 5364  recexsrlem 5366  addgt0sr 5367  sqgt0sr 5369  ssgt0sr 5371  mappsrpr 5372  ltpsrpr 5373  map2psrpr 5374  suppsr2 5377  suppsr3 5378  supsrlem1 5379  supsrlem2 5380  supsrlem3 5381  supsrlem5 5383  opelreal 5403  elreal 5404  eqresr 5409  mulresr 5411  axicn 5424  axmulass 5432  ax1ne0 5434  axi2m1 5439  axcnre 5440  pre-axmulgt0 5444  elxr 5689  ssxr 5694  1nn 6079  nn1suc 6084  xrsupss 6246  xrinfmss 6247  elnn0 6269  nn0ssz 6320  nn0ind-raph 6385  seq1lem1 6674  seq11lem 6680  expval 6765  facnn 7136  fac0 7137  bcval 7161  serz0 7256  serzcmp0 7258  binomlem1 7269  binomlem4 7272  binomlem6 7274  climuni 7302  climuz0i 7311  serzclim0 7312  climaddci 7335  iserzcmp0 7346  caucvg3 7371  ser1f0i 7373  ser1consti 7374  ser1clim0 7376  ser1cmp0i 7378  cvgcmpubi 7389  cvgcmp3cetlem1 7392  cvgcmp3cetlem2 7393  isumnn0nnai 7412  infcvgaux1i 7423  infcvglem2 7426  infcvglem3 7427  explecnv 7438  geolimilem 7440  efseq1ex 7511  dfef2i 7512  erelem2 7525  erelem4 7527  ele3lem 7531  ege2le3lem2 7534  ef0 7540  acdc2lem2 7701  acdc5lem2 7704  xpnnen 7711  ruclem6 7727  ruclem7 7728  ruclem8 7729  ruclem39 7760  infmap1 7785  infmap2 7793  dscmet 8129  fsumcnlem 8200  grpidvallem 8274  ipval2 8611  minveclem30 8834  minveclem31 8835  hhph 9321  hlim0 9381  hlimcaui 9383  hlimunii 9385  hsn0elch 9396  elch0 9402  occllem6 9454  occllem7 9455  projlem17 9478  projlem31 9492  choc0 9566  shintcli 9569  shincli 9607  chincli 9659  h1deoi 9748  h1de2ctlem 9754  spansni 9756  osumlem5 9860  pjfni 9924  df0op2 9958  ho01i 10034  0cnfn 10183  0lnfn 10188  nmfn0 10190  nmop0h 10195  nmopun 10218  lnfnconi 10269  pjnmopi 10355  atoml2i 10592  cdj3lem2 10644  f1fi 10779  domleqt 10792  unpde2eg22 10826  definc 10869  seqzp2 10918  fora1 10952  zrdivrng 10969  eqindhome 11047  top2usne 11051  clindistop 11131  intopcon 11133  sdc 11877  fsumleisumi 11889  trirn 11897  heiborlem3 12013  heiborlem5 12015  heiborlem7 12017  heiborlem8 12018  heiborlem18 12028  heiborlem20 12030  heiborlem25 12035  heiborlem26 12036  heiborlem29 12039  heiborlem40 12050  bfplem1 12054  bfplem2 12055  bfplem3 12056  bfplem8 12061  bfplem11 12064  bfp 12065  ismrer1 12080

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 999  ax-12 1004  ax-17 1007  ax-4 1009  ax-5o 1011  ax-6o 1014  ax-9o 1159  ax-ext 1500

This theorem depends on definitions:  df-bi 145  df-an 223  df-ex 1017  df-sb 1209  df-clab 1506  df-cleq 1511  df-clel 1514  df-v 1858

Copyright terms: Public domain