Theorem elisseti 1818

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

Syntax hints:   e. wcel 958  Vcvv 1811

This theorem is referenced by:  onunisuc 3106  tz7.44-2 3929  tz7.44-3 3930  caoprmo 4070  oe0 4161  oev2 4162  oneo 4212  endisj 4437  pw2en 4446  pwen 4503  0sdom1dom 4525  pwfiOLD 4571  pm54.43 4572  rankxplim3 4714  unxpdom2 4845  sucxpdom 4846  cfsuc 4915  uncdadom 4921  cdaun 4922  pm110.643 4923  cdaen 4924  cda1en 4926  cdacomen 4929  cdaassen 4930  mapcdaen 4932  nlt1pi 5033  indpi 5034  1qec 5068  mulidpq 5069  1lt2pq 5078  ltaddpq 5079  halfpq 5082  ltrpq 5085  1pr 5117  addclprlem1 5118  1idpr 5133  prlem934a 5137  prlem934b 5138  prlem936 5155  reclem3pr 5158  reclem4pr 5159  gt0srpr 5187  m1p1sr 5201  m1m1sr 5202  0lt1sr 5204  0idsr 5206  1idsr 5207  pn0sr 5210  recexsrlem 5212  addgt0sr 5213  sqgt0sr 5215  ssgt0sr 5217  mappsrpr 5218  ltpsrpr 5219  map2psrpr 5220  suppsr2 5223  suppsr3 5224  supsrlem1 5225  supsrlem2 5226  supsrlem3 5227  supsrlem5 5229  opelreal 5249  elreal 5250  eqresr 5255  mulresr 5257  axicn 5270  axmulass 5278  ax1ne0 5280  axi2m1 5285  axcnre 5286  pre-axmulgt0 5290  elxr 5535  ssxr 5540  1nn 5934  nn1suc 5939  xrsupss 6078  xrinfmss 6079  elnn0 6101  nn0ssz 6152  nn0ind-raph 6214  seq1lem1 6309  seq11lem 6315  expvalt 6570  facnnt 6933  fac0 6934  bcvalt 6958  serz0 7053  serzcmp0 7055  binomlem1 7066  binomlem4 7069  binomlem6 7071  climuni 7099  climuz0 7108  serzclim0 7109  climaddc 7132  iserzcmp0 7143  caucvg3t 7168  ser1const 7171  ser1clim0 7173  ser1cmp0 7175  cvgcmpub 7185  cvgcmp3cetlem1 7188  cvgcmp3cetlem2 7189  isumnn0nna 7208  infcvgaux1 7219  infcvglem2 7222  infcvglem3 7223  geolimilem 7235  efseq1ex 7306  dfef2 7307  erelem2 7320  erelem4 7322  ele3lem 7326  ege2le3lem2 7329  ef0 7335  acdc2lem2 7489  acdc5lem2 7492  xpnnen 7499  ruclem6 7515  ruclem7 7516  ruclem8 7517  ruclem39 7548  infmap1 7573  infmap2 7581  dscmet 7918  fsumcnlem 7989  ipval2 8357  minveclem30 8574  minveclem31 8575  hhph 9045  hlim0 9105  hlimcau 9107  hlimuni 9109  hsn0elch 9120  elch0 9126  occllem6 9178  occllem7 9179  projlem17 9202  projlem31 9216  choc0 9290  shintcl 9293  shincl 9331  chincl 9383  h1deot 9472  h1de2ctlem 9478  spansn 9480  osumlem5 9582  pjfn 9646  df0op2 9678  ho01 9754  0cnfn 9904  0lnfn 9909  nmfn0 9911  nmop0h 9916  nmopunt 9939  lnfncon 9990  pjnmop 10075  atoml2 10310  cdj3lem2 10362  boe 10460  eqindhome 10541  top2usne 10549

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 963  ax-12 968  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-ext 1459

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 981  df-sb 1172  df-clab 1464  df-cleq 1469  df-clel 1472  df-v 1812

Copyright terms: Public domain