Theorem onss 7833

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2147   ⊆ wss 3900  Ord word 6387  Oncon0 6388

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-sep 5255  ax-pr 5398

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ne 2960  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-pss 4017  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4841  df-uni 4873  df-br 5109  df-opab 5174  df-tr 5219  df-eprel 5558  df-po 5566  df-so 5567  df-fr 5611  df-we 5613  df-ord 6391  df-on 6392

This theorem is used by:  onuni  7836  onminex  7850  onssi  7883  tfi  7898  soseq  8213  tfr3  8445  tz7.49  8493  tz7.49c  8494  oacomf1olem  8610  oeeulem  8648  cofonr  8721  naddcllem  8723  naddov2  8726  naddunif  8741  naddasslem1  8742  naddasslem2  8743  ordtypelem2  9550  cantnfcl  9705  cantnflt  9710  cantnfp1lem3  9718  oemapvali  9722  cantnflem1c  9725  cantnflem1d  9726  cantnflem1  9727  cantnf  9731  cnfcom  9738  cnfcom3lem  9741  infxpenlem  10131  ac10ct  10152  dfac12lem1  10261  dfac12lem2  10262  cfeq0  10373  cfsuc  10374  cff1  10375  cfflb  10376  cofsmo  10386  cfsmolem  10387  alephsing  10393  zorn2lem2  10614  ttukeylem3  10628  ttukeylem5  10630  ttukeylem6  10631  inar1  10899  nosupno  28117  elold  28302  madefi  28356  oldfi  28357  oldfib  28820  dfac15  35886  fnlfvk30  36068  fnlfvk3n0  36069  nmulrid  37161  ltnadd  37182  naddle  37183  ontgval  37434  aomclem6  44327  tfsconcatlem  44599  tfsconcatfv  44604  ofoafo  44619  ofoaid1  44621  ofoaid2  44622  dfno2  44690