Theorem onss 7797

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145   ⊆ wss 3899  Ord word 6360  Oncon0 6361

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733  ax-sep 5249  ax-pr 5391

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 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-tr 5213  df-eprel 5551  df-po 5559  df-so 5560  df-fr 5604  df-we 5606  df-ord 6364  df-on 6365

This theorem is used by:  onuni  7800  onminex  7814  onssi  7847  tfi  7862  soseq  8169  tfr3  8400  tz7.49  8448  tz7.49c  8449  oacomf1olem  8565  oeeulem  8603  cofonr  8676  naddcllem  8678  naddov2  8681  naddunif  8696  naddasslem1  8697  naddasslem2  8698  ordtypelem2  9506  cantnfcl  9661  cantnflt  9666  cantnfp1lem3  9674  oemapvali  9678  cantnflem1c  9681  cantnflem1d  9682  cantnflem1  9683  cantnf  9687  cnfcom  9694  cnfcom3lem  9697  infxpenlem  10085  ac10ct  10106  dfac12lem1  10215  dfac12lem2  10216  cfeq0  10327  cfsuc  10328  cff1  10329  cfflb  10330  cofsmo  10340  cfsmolem  10341  alephsing  10347  zorn2lem2  10568  ttukeylem3  10582  ttukeylem5  10584  ttukeylem6  10585  inar1  10853  nosupno  28053  elold  28238  madefi  28292  oldfi  28293  oldfib  28756  nmulrid  36926  ltnadd  36947  naddle  36948  ontgval  37199  aomclem6  44045  tfsconcatlem  44322  tfsconcatfv  44327  ofoafo  44342  ofoaid1  44344  ofoaid2  44345  dfno2  44413