Theorem onss 7804

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 6396	. 2 ⊢ (𝐴 ∈ On → Ord 𝐴)
2		ordsson 7802	. 2 ⊢ (Ord 𝐴 → 𝐴 ⊆ On)
3	1, 2	syl 17	1 ⊢ (𝐴 ∈ On → 𝐴 ⊆ On)

Syntax hints:   → wi 4   ∈ wcel 2106   ⊆ wss 3963  Ord word 6385  Oncon0 6386

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706  ax-sep 5302  ax-nul 5312  ax-pr 5438

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-ne 2939  df-ral 3060  df-rex 3069  df-rab 3434  df-v 3480  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-pss 3983  df-nul 4340  df-if 4532  df-pw 4607  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-br 5149  df-opab 5211  df-tr 5266  df-eprel 5589  df-po 5597  df-so 5598  df-fr 5641  df-we 5643  df-ord 6389  df-on 6390

This theorem is referenced by:  predonOLD  7806  onuni  7808  onminex  7822  sucexeloniOLD  7830  suceloniOLD  7832  onssi  7858  tfi  7874  soseq  8183  tfr3  8438  tz7.49  8484  tz7.49c  8485  oacomf1olem  8601  oeeulem  8638  cofonr  8711  naddcllem  8713  naddov2  8716  naddunif  8730  naddasslem1  8731  naddasslem2  8732  ordtypelem2  9557  cantnfcl  9705  cantnflt  9710  cantnfp1lem3  9718  oemapvali  9722  cantnflem1c  9725  cantnflem1d  9726  cantnflem1  9727  cantnf  9731  cnfcom  9738  cnfcom3lem  9741  infxpenlem  10051  ac10ct  10072  dfac12lem1  10182  dfac12lem2  10183  cfeq0  10294  cfsuc  10295  cff1  10296  cfflb  10297  cofsmo  10307  cfsmolem  10308  alephsing  10314  zorn2lem2  10535  ttukeylem3  10549  ttukeylem5  10551  ttukeylem6  10552  inar1  10813  nosupno  27763  elold  27923  madefi  27965  oldfi  27966  ontgval  36414  aomclem6  43048  tfsconcatlem  43326  tfsconcatfv  43331  ofoafo  43346  ofoaid1  43348  ofoaid2  43349  dfno2  43418