Theorem elisseti 1814

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

Syntax hints:   e. wcel 956  Vcvv 1807

This theorem is referenced by:  onunisuc 3101  tz7.44-2 3920  tz7.44-3 3921  caoprmo 4062  oe0 4151  oev2 4152  oneo 4202  endisj 4423  pw2en 4432  pwen 4489  0sdom1dom 4510  pwfi 4551  pm54.43 4552  rankxplim3 4694  unxpdom2 4825  sucxpdom 4826  cfsuc 4895  uncdadom 4901  cdaun 4902  pm110.643 4903  cdaen 4904  cda1en 4906  cdacomen 4909  cdaassen 4910  mapcdaen 4912  nlt1pi 5013  indpi 5014  1qec 5048  mulidpq 5049  1lt2pq 5058  ltaddpq 5059  halfpq 5062  ltrpq 5065  1pr 5097  addclprlem1 5098  1idpr 5113  prlem934a 5117  prlem934b 5118  prlem936 5135  reclem3pr 5138  reclem4pr 5139  gt0srpr 5167  m1p1sr 5181  m1m1sr 5182  0lt1sr 5184  0idsr 5186  1idsr 5187  pn0sr 5190  recexsrlem 5192  addgt0sr 5193  sqgt0sr 5195  ssgt0sr 5197  mappsrpr 5198  ltpsrpr 5199  map2psrpr 5200  suppsr2 5203  suppsr3 5204  supsrlem1 5205  supsrlem2 5206  supsrlem3 5207  supsrlem5 5209  opelreal 5229  elreal 5230  eqresr 5235  mulresr 5237  axicn 5250  axmulass 5258  ax1ne0 5260  axi2m1 5265  axcnre 5266  pre-axmulgt0 5270  elxr 5516  ssxr 5521  1nn 5890  nn1suc 5895  xrsupss 6033  xrinfmss 6034  elnn0 6056  nn0ssz 6107  nn0ind-raph 6170  seq1lem1 6254  seq11lem 6260  expvalt 6510  facnnt 6878  fac0 6879  bcvalt 6903  serz0 6999  serzcmp0 7001  binomlem1 7012  binomlem4 7015  binomlem6 7017  climuni 7044  climuz0 7053  serzclim0 7054  climaddc 7076  iserzcmp0 7087  caucvg3t 7112  ser1const 7115  ser1clim0 7117  ser1cmp0 7119  cvgcmpub 7129  cvgcmp3cetlem1 7132  cvgcmp3cetlem2 7133  isumnn0nna 7151  infcvgaux1 7162  infcvglem2 7165  infcvglem3 7166  geolimilem 7178  efseq1ex 7256  dfef2 7257  erelem2 7270  erelem4 7272  ele3lem 7276  ege2le3lem2 7279  ef0 7285  acdc2lem2 7439  acdc5lem2 7442  xpnnen 7449  ruclem6 7466  ruclem7 7467  ruclem8 7468  ruclem39 7499  infmap1 7524  infmap2 7531  dscmet 7870  fsumcnlem 7939  ipval2 8304  minveclem30 8518  minveclem31 8519  hhph 8984  hlim0 9044  hlimcau 9046  hlimuni 9048  hsn0elch 9059  elch0 9065  occllem6 9117  occllem7 9118  projlem17 9141  projlem31 9155  choc0 9228  shintcl 9231  shincl 9269  chincl 9321  h1deot 9410  h1de2ctlem 9417  spansn 9419  osumlem5 9522  pjfn 9586  df0op2 9618  ho01 9694  0cnfn 9843  0lnfn 9848  nmfn0 9850  nmop0h 9854  nmopunt 9877  lnfncon 9928  pjnmop 10013  atoml2 10247  cdj3lem2 10296  boe 10392

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 961  ax-12 966  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-ext 1457

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 979  df-sb 1170  df-clab 1462  df-cleq 1467  df-clel 1470  df-v 1808

Copyright terms: Public domain