Theorem onss 7741

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

Syntax hints:   → wi 4   ∈ wcel 2109   ⊆ wss 3911  Ord word 6319  Oncon0 6320

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5246  ax-nul 5256  ax-pr 5382

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-ral 3045  df-rex 3054  df-rab 3403  df-v 3446  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-pss 3931  df-nul 4293  df-if 4485  df-pw 4561  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5103  df-opab 5165  df-tr 5210  df-eprel 5531  df-po 5539  df-so 5540  df-fr 5584  df-we 5586  df-ord 6323  df-on 6324

This theorem is referenced by:  onuni  7744  onminex  7758  sucexeloniOLD  7766  onssi  7793  tfi  7809  soseq  8115  tfr3  8344  tz7.49  8390  tz7.49c  8391  oacomf1olem  8505  oeeulem  8542  cofonr  8615  naddcllem  8617  naddov2  8620  naddunif  8634  naddasslem1  8635  naddasslem2  8636  ordtypelem2  9448  cantnfcl  9596  cantnflt  9601  cantnfp1lem3  9609  oemapvali  9613  cantnflem1c  9616  cantnflem1d  9617  cantnflem1  9618  cantnf  9622  cnfcom  9629  cnfcom3lem  9632  infxpenlem  9942  ac10ct  9963  dfac12lem1  10073  dfac12lem2  10074  cfeq0  10185  cfsuc  10186  cff1  10187  cfflb  10188  cofsmo  10198  cfsmolem  10199  alephsing  10205  zorn2lem2  10426  ttukeylem3  10440  ttukeylem5  10442  ttukeylem6  10443  inar1  10704  nosupno  27591  elold  27757  madefi  27800  oldfi  27801  ontgval  36392  aomclem6  43021  tfsconcatlem  43298  tfsconcatfv  43303  ofoafo  43318  ofoaid1  43320  ofoaid2  43321  dfno2  43390