Theorem onss 7784

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 6367	. 2 ⊢ (𝐴 ∈ On → Ord 𝐴)
2		ordsson 7782	. 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 6356  Oncon0 6357

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 2732  ax-sep 5251  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 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  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 5555  df-po 5563  df-so 5564  df-fr 5608  df-we 5610  df-ord 6360  df-on 6361

This theorem is used by:  onuni  7787  onminex  7801  onssi  7834  tfi  7849  soseq  8157  tfr3  8388  tz7.49  8434  tz7.49c  8435  oacomf1olem  8551  oeeulem  8589  cofonr  8662  naddcllem  8664  naddov2  8667  naddunif  8682  naddasslem1  8683  naddasslem2  8684  ordtypelem2  9491  cantnfcl  9646  cantnflt  9651  cantnfp1lem3  9659  oemapvali  9663  cantnflem1c  9666  cantnflem1d  9667  cantnflem1  9668  cantnf  9672  cnfcom  9679  cnfcom3lem  9682  infxpenlem  10016  ac10ct  10037  dfac12lem1  10146  dfac12lem2  10147  cfeq0  10258  cfsuc  10259  cff1  10260  cfflb  10261  cofsmo  10271  cfsmolem  10272  alephsing  10278  zorn2lem2  10499  ttukeylem3  10513  ttukeylem5  10515  ttukeylem6  10516  inar1  10784  nosupno  27939  elold  28124  madefi  28178  oldfi  28179  oldfib  28642  nmulrid  36777  ltnadd  36798  naddle  36799  ontgval  37050  aomclem6  43900  tfsconcatlem  44177  tfsconcatfv  44182  ofoafo  44197  ofoaid1  44199  ofoaid2  44200  dfno2  44268