Theorem onss 7727

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

Syntax hints:   → wi 4   ∈ wcel 2113   ⊆ wss 3898  Ord word 6313  Oncon0 6314

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705  ax-sep 5238  ax-nul 5248  ax-pr 5374

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-ne 2930  df-ral 3049  df-rex 3058  df-rab 3397  df-v 3439  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-pss 3918  df-nul 4283  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4861  df-br 5096  df-opab 5158  df-tr 5203  df-eprel 5521  df-po 5529  df-so 5530  df-fr 5574  df-we 5576  df-ord 6317  df-on 6318

This theorem is referenced by:  onuni  7730  onminex  7744  onssi  7777  tfi  7792  soseq  8098  tfr3  8327  tz7.49  8373  tz7.49c  8374  oacomf1olem  8488  oeeulem  8525  cofonr  8598  naddcllem  8600  naddov2  8603  naddunif  8617  naddasslem1  8618  naddasslem2  8619  ordtypelem2  9416  cantnfcl  9568  cantnflt  9573  cantnfp1lem3  9581  oemapvali  9585  cantnflem1c  9588  cantnflem1d  9589  cantnflem1  9590  cantnf  9594  cnfcom  9601  cnfcom3lem  9604  infxpenlem  9915  ac10ct  9936  dfac12lem1  10046  dfac12lem2  10047  cfeq0  10158  cfsuc  10159  cff1  10160  cfflb  10161  cofsmo  10171  cfsmolem  10172  alephsing  10178  zorn2lem2  10399  ttukeylem3  10413  ttukeylem5  10415  ttukeylem6  10416  inar1  10677  nosupno  27662  elold  27834  madefi  27878  oldfi  27879  ontgval  36547  aomclem6  43216  tfsconcatlem  43493  tfsconcatfv  43498  ofoafo  43513  ofoaid1  43515  ofoaid2  43516  dfno2  43585