Theorem elisseti 1355

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

Syntax hints:   e. wcel 1092  Vcvv 1348

This theorem is referenced by:  onunisuc 2354  onuninsuc 2356  tz7.44-2 2967  tz7.44-3 2968  caoprmo 3084  oe0 3130  pw2en 3348  pwen 3398  0sdom1dom 3420  unxpdom2 3651  sucxpdom 3652  cfsuc 3709  uncdadom 3718  cdaen 3719  cda1en 3721  cdacomen 3724  cdaassen 3725  nlt1pi 3827  indpi 3828  1qec 3862  mulidpq 3863  1lt2pq 3872  ltaddpq 3873  halfpq 3876  ltrpq 3879  1pr 3911  addclprlem1 3912  1idpr 3927  prlem934a 3931  prlem934b 3932  prlem936 3949  reclem3pr 3952  reclem4pr 3953  gt0srpr 3981  m1p1sr 3995  m1m1sr 3996  0lt1sr 3998  0idsr 4000  1idsr 4001  pn0sr 4004  recexsrlem 4006  addgt0sr 4007  sqgt0sr 4009  ssgt0sr 4011  mappsrpr 4012  ltpsrpr 4013  map2psrpr 4014  suppsr2 4017  suppsr3 4018  supsrlem1 4019  supsrlem2 4020  supsrlem3 4021  supsrlem5 4023  opelreal 4043  elreal 4044  eqresr 4049  mulresr 4051  axicn 4065  axmulass 4073  ax1ne0 4075  axrecex 4079  axi2m1 4082  axmulgt0 4086  axcnre 4087  divval 4217  1nn 4432  nnind 4434  nn1suc 4435  elnn0 4536  nn0ssz 4578  nn0ind 4612  seqlem1 4662  seqlem2 4663  seq1lem 4668  facnnt 4870  fac0 4871  clim0 4882  climuni 4884  ruclem6 4890  ruclem7 4891  ruclem39 4923  xpnnen 4927  infunabs 4946  infcdaabs 4947  infmap1 4950  hlim0 5140  hlimcau 5142  hlimuni 5144  hsn0elch 5155  elch0 5158  occllem6 5185  occllem7 5186  projlem17 5209  projlem26 5218  projlem31 5223  choc0 5291  shintcl 5294  shincl 5332  chincl 5382  h1deot 5454  h1de2ctlem 5460  spansn 5462  osumlem5 5534  pjfn 5586  ho0 5612

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-gen 677  ax-9 799  ax-12 802  ax-17 925  ax-ext 1074

This theorem depends on definitions:  df-bi 128  df-an 198  df-ex 679  df-sb 853  df-clab 1093  df-cleq 1097  df-clel 1099  df-v 1349

metamath.org