Theorem onss 7790

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146   ⊆ wss 3906  Ord word 6363  Oncon0 6364

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 2148  ax-9 2156  ax-ext 2737  ax-sep 5259  ax-pr 5406

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 2744  df-cleq 2757  df-clel 2840  df-ne 2961  df-ral 3082  df-rex 3092  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-pss 3926  df-nul 4287  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-opab 5176  df-tr 5221  df-eprel 5563  df-po 5571  df-so 5572  df-fr 5616  df-we 5618  df-ord 6367  df-on 6368

This theorem is used by:  onuni  7793  onminex  7807  onssi  7840  tfi  7855  soseq  8161  tfr3  8392  tz7.49  8438  tz7.49c  8439  oacomf1olem  8555  oeeulem  8593  cofonr  8666  naddcllem  8668  naddov2  8671  naddunif  8686  naddasslem1  8687  naddasslem2  8688  ordtypelem2  9488  cantnfcl  9643  cantnflt  9648  cantnfp1lem3  9656  oemapvali  9660  cantnflem1c  9663  cantnflem1d  9664  cantnflem1  9665  cantnf  9669  cnfcom  9676  cnfcom3lem  9679  infxpenlem  10013  ac10ct  10034  dfac12lem1  10143  dfac12lem2  10144  cfeq0  10255  cfsuc  10256  cff1  10257  cfflb  10258  cofsmo  10268  cfsmolem  10269  alephsing  10275  zorn2lem2  10496  ttukeylem3  10510  ttukeylem5  10512  ttukeylem6  10513  inar1  10775  nosupno  27918  elold  28103  madefi  28157  oldfi  28158  oldfib  28621  nmulrid  36726  ltnadd  36747  naddle  36748  ontgval  36999  aomclem6  43844  tfsconcatlem  44121  tfsconcatfv  44126  ofoafo  44141  ofoaid1  44143  ofoaid2  44144  dfno2  44212