Theorem onss 7721

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

Syntax hints:   → wi 4   ∈ wcel 2109   ⊆ wss 3903  Ord word 6306  Oncon0 6307

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 5235  ax-nul 5245  ax-pr 5371

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 3395  df-v 3438  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-pss 3923  df-nul 4285  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-br 5093  df-opab 5155  df-tr 5200  df-eprel 5519  df-po 5527  df-so 5528  df-fr 5572  df-we 5574  df-ord 6310  df-on 6311

This theorem is referenced by:  onuni  7724  onminex  7738  onssi  7771  tfi  7786  soseq  8092  tfr3  8321  tz7.49  8367  tz7.49c  8368  oacomf1olem  8482  oeeulem  8519  cofonr  8592  naddcllem  8594  naddov2  8597  naddunif  8611  naddasslem1  8612  naddasslem2  8613  ordtypelem2  9411  cantnfcl  9563  cantnflt  9568  cantnfp1lem3  9576  oemapvali  9580  cantnflem1c  9583  cantnflem1d  9584  cantnflem1  9585  cantnf  9589  cnfcom  9596  cnfcom3lem  9599  infxpenlem  9907  ac10ct  9928  dfac12lem1  10038  dfac12lem2  10039  cfeq0  10150  cfsuc  10151  cff1  10152  cfflb  10153  cofsmo  10163  cfsmolem  10164  alephsing  10170  zorn2lem2  10391  ttukeylem3  10405  ttukeylem5  10407  ttukeylem6  10408  inar1  10669  nosupno  27613  elold  27783  madefi  27827  oldfi  27828  ontgval  36405  aomclem6  43032  tfsconcatlem  43309  tfsconcatfv  43314  ofoafo  43329  ofoaid1  43331  ofoaid2  43332  dfno2  43401