Theorem onss 7792

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

Syntax hints:   → wi 4   ∈ wcel 2098   ⊆ wss 3946  Ord word 6374  Oncon0 6375

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696  ax-sep 5303  ax-nul 5310  ax-pr 5432

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-ne 2930  df-ral 3051  df-rex 3060  df-rab 3419  df-v 3463  df-dif 3949  df-un 3951  df-in 3953  df-ss 3963  df-pss 3966  df-nul 4325  df-if 4533  df-pw 4608  df-sn 4633  df-pr 4635  df-op 4639  df-uni 4913  df-br 5153  df-opab 5215  df-tr 5270  df-eprel 5585  df-po 5593  df-so 5594  df-fr 5636  df-we 5638  df-ord 6378  df-on 6379

This theorem is referenced by:  predonOLD  7794  onuni  7796  onminex  7810  sucexeloniOLD  7818  suceloniOLD  7820  onssi  7846  tfi  7862  soseq  8172  tfr3  8428  tz7.49  8474  tz7.49c  8475  oacomf1olem  8593  oeeulem  8630  cofonr  8703  naddcllem  8705  naddov2  8708  naddunif  8722  naddasslem1  8723  naddasslem2  8724  ordtypelem2  9558  cantnfcl  9706  cantnflt  9711  cantnfp1lem3  9719  oemapvali  9723  cantnflem1c  9726  cantnflem1d  9727  cantnflem1  9728  cantnf  9732  cnfcom  9739  cnfcom3lem  9742  infxpenlem  10052  ac10ct  10073  dfac12lem1  10182  dfac12lem2  10183  cfeq0  10295  cfsuc  10296  cff1  10297  cfflb  10298  cofsmo  10308  cfsmolem  10309  alephsing  10315  zorn2lem2  10536  ttukeylem3  10550  ttukeylem5  10552  ttukeylem6  10553  inar1  10814  nosupno  27725  elold  27885  ontgval  36091  aomclem6  42657  tfsconcatlem  42939  tfsconcatfv  42944  ofoafo  42959  ofoaid1  42961  ofoaid2  42962  dfno2  43032