HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Theorem elisseti 1809
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
StepHypRef Expression
1 elisseti.1 . 2 |- A e. B
2 elisset 1808 . 2 |- (A e. B -> A e. V)
31, 2ax-mp 7 1 |- A e. V
Colors of variables: wff set class
Syntax hints:   e. wcel 955  Vcvv 1802
This theorem is referenced by:  onunisuc 3096  tz7.44-2 3914  tz7.44-3 3915  caoprmo 4056  oe0 4145  oev2 4146  oneo 4196  endisj 4417  pw2en 4426  pwen 4483  0sdom1dom 4504  pwfi 4545  pm54.43 4546  rankxplim3 4686  unxpdom2 4817  sucxpdom 4818  cfsuc 4887  uncdadom 4893  cdaun 4894  pm110.643 4895  cdaen 4896  cda1en 4898  cdacomen 4901  cdaassen 4902  mapcdaen 4904  nlt1pi 5005  indpi 5006  1qec 5040  mulidpq 5041  1lt2pq 5050  ltaddpq 5051  halfpq 5054  ltrpq 5057  1pr 5089  addclprlem1 5090  1idpr 5105  prlem934a 5109  prlem934b 5110  prlem936 5127  reclem3pr 5130  reclem4pr 5131  gt0srpr 5159  m1p1sr 5173  m1m1sr 5174  0lt1sr 5176  0idsr 5178  1idsr 5179  pn0sr 5182  recexsrlem 5184  addgt0sr 5185  sqgt0sr 5187  ssgt0sr 5189  mappsrpr 5190  ltpsrpr 5191  map2psrpr 5192  suppsr2 5195  suppsr3 5196  supsrlem1 5197  supsrlem2 5198  supsrlem3 5199  supsrlem5 5201  opelreal 5221  elreal 5222  eqresr 5227  mulresr 5229  axicn 5242  axmulass 5250  ax1ne0 5252  axi2m1 5257  axcnre 5258  pre-axmulgt0 5262  elxr 5508  ssxr 5513  1nn 5882  nn1suc 5887  xrsupss 6025  xrinfmss 6026  elnn0 6048  nn0ssz 6099  nn0ind-raph 6162  seq1lem1 6246  seq11lem 6252  expvalt 6502  facnnt 6870  fac0 6871  bcvalt 6895  serz0 6991  serzcmp0 6993  binomlem1 7004  binomlem4 7007  binomlem6 7009  climuni 7036  climuz0 7045  serzclim0 7046  climaddc 7068  iserzcmp0 7079  caucvg3t 7104  ser1const 7107  ser1clim0 7109  ser1cmp0 7111  cvgcmpub 7121  cvgcmp3cetlem1 7124  cvgcmp3cetlem2 7125  isumnn0nna 7143  infcvgaux1 7154  infcvglem2 7157  infcvglem3 7158  geolimilem 7170  efseq1ex 7248  dfef2 7249  erelem2 7262  erelem4 7264  ele3lem 7268  ege2le3lem2 7271  ef0 7277  acdc2lem2 7431  acdc5lem2 7434  xpnnen 7441  ruclem6 7458  ruclem7 7459  ruclem8 7460  ruclem39 7491  infmap1 7516  infmap2 7523  dscmet 7856  fsumcnlem 7923  ipval2 8291  minveclem30 8505  minveclem31 8506  hhph 8966  hlim0 9026  hlimcau 9028  hlimuni 9030  hsn0elch 9041  elch0 9047  occllem6 9094  occllem7 9095  projlem17 9118  projlem31 9132  choc0 9205  shintcl 9208  shincl 9246  chincl 9298  h1deot 9387  h1de2ctlem 9394  spansn 9396  osumlem5 9499  pjfn 9563  df0op2 9595  ho01 9671  0cnfn 9820  0lnfn 9825  nmfn0 9827  nmop0h 9831  nmopunt 9854  lnfncon 9905  pjnmop 9986  atoml2 10218  cdj3lem2 10267  boe 10356
This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 960  ax-12 965  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975  ax-9o 1119  ax-ext 1452
This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 978  df-sb 1168  df-clab 1457  df-cleq 1462  df-clel 1465  df-v 1803
Copyright terms: Public domain