Theorem onss 7768

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

Syntax hints:   → wi 4   ∈ wcel 2142   ⊆ wss 3904  Ord word 6345  Oncon0 6346

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734  ax-sep 5246  ax-pr 5390

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1099  df-3an 1100  df-tru 1563  df-fal 1573  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-ne 2958  df-ral 3077  df-rex 3087  df-rab 3415  df-v 3456  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-pss 3924  df-nul 4286  df-if 4481  df-pw 4557  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-tr 5208  df-eprel 5547  df-po 5555  df-so 5556  df-fr 5600  df-we 5602  df-ord 6349  df-on 6350

This theorem is referenced by:  onuni  7771  onminex  7785  onssi  7818  tfi  7833  soseq  8139  tfr3  8370  tz7.49  8416  tz7.49c  8417  oacomf1olem  8533  oeeulem  8571  cofonr  8644  naddcllem  8646  naddov2  8649  naddunif  8664  naddasslem1  8665  naddasslem2  8666  ordtypelem2  9467  cantnfcl  9622  cantnflt  9627  cantnfp1lem3  9635  oemapvali  9639  cantnflem1c  9642  cantnflem1d  9643  cantnflem1  9644  cantnf  9648  cnfcom  9655  cnfcom3lem  9658  infxpenlem  9969  ac10ct  9990  dfac12lem1  10100  dfac12lem2  10101  cfeq0  10213  cfsuc  10214  cff1  10215  cfflb  10216  cofsmo  10226  cfsmolem  10227  alephsing  10233  zorn2lem2  10454  ttukeylem3  10468  ttukeylem5  10470  ttukeylem6  10471  inar1  10733  nosupno  27764  elold  27949  madefi  28003  oldfi  28004  oldfib  28467  ontgval  36788  aomclem6  43633  tfsconcatlem  43910  tfsconcatfv  43915  ofoafo  43930  ofoaid1  43932  ofoaid2  43933  dfno2  44001