Theorem onss 7783

Description: An ordinal number is a subset of the class of ordinal numbers. (Contributed by NM, 5-Jun-1994.)

Assertion

Ref	Expression
onss	⊢ (𝐴 ∈ On → 𝐴 ⊆ On)

Proof of Theorem onss

Step	Hyp	Ref	Expression
1		eloni 6371	. 2 ⊢ (𝐴 ∈ On → Ord 𝐴)
2		ordsson 7781	. 2 ⊢ (Ord 𝐴 → 𝐴 ⊆ On)
3	1, 2	syl 18	1 ⊢ (𝐴 ∈ On → 𝐴 ⊆ On)

Syntax hints:   → wi 4   ∈ wcel 2149   ⊆ wss 3913  Ord word 6360  Oncon0 6361

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741  ax-sep 5261  ax-pr 5405

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-ne 2965  df-ral 3086  df-rex 3096  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-pss 3933  df-nul 4295  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4877  df-br 5114  df-opab 5178  df-tr 5223  df-eprel 5562  df-po 5570  df-so 5571  df-fr 5615  df-we 5617  df-ord 6364  df-on 6365

This theorem is referenced by:  onuni  7786  onminex  7800  onssi  7833  tfi  7848  soseq  8154  tfr3  8385  tz7.49  8431  tz7.49c  8432  oacomf1olem  8548  oeeulem  8586  cofonr  8659  naddcllem  8661  naddov2  8664  naddunif  8679  naddasslem1  8680  naddasslem2  8681  ordtypelem2  9480  cantnfcl  9635  cantnflt  9640  cantnfp1lem3  9648  oemapvali  9652  cantnflem1c  9655  cantnflem1d  9656  cantnflem1  9657  cantnf  9661  cnfcom  9668  cnfcom3lem  9671  infxpenlem  9996  ac10ct  10017  dfac12lem1  10126  dfac12lem2  10127  cfeq0  10239  cfsuc  10240  cff1  10241  cfflb  10242  cofsmo  10252  cfsmolem  10253  alephsing  10259  zorn2lem2  10480  ttukeylem3  10494  ttukeylem5  10496  ttukeylem6  10497  inar1  10759  nosupno  27832  elold  28017  madefi  28071  oldfi  28072  oldfib  28535  ontgval  36830  aomclem6  43677  tfsconcatlem  43954  tfsconcatfv  43959  ofoafo  43974  ofoaid1  43976  ofoaid2  43977  dfno2  44045