Theorem onss 7788

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

Syntax hints:   → wi 4   ∈ wcel 2107   ⊆ wss 3933  Ord word 6364  Oncon0 6365

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2706  ax-sep 5278  ax-nul 5288  ax-pr 5414

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-sb 2064  df-clab 2713  df-cleq 2726  df-clel 2808  df-ne 2932  df-ral 3051  df-rex 3060  df-rab 3421  df-v 3466  df-dif 3936  df-un 3938  df-in 3940  df-ss 3950  df-pss 3953  df-nul 4316  df-if 4508  df-pw 4584  df-sn 4609  df-pr 4611  df-op 4615  df-uni 4890  df-br 5126  df-opab 5188  df-tr 5242  df-eprel 5566  df-po 5574  df-so 5575  df-fr 5619  df-we 5621  df-ord 6368  df-on 6369

This theorem is referenced by:  onuni  7791  onminex  7805  sucexeloniOLD  7813  suceloniOLD  7815  onssi  7841  tfi  7857  soseq  8167  tfr3  8422  tz7.49  8468  tz7.49c  8469  oacomf1olem  8585  oeeulem  8622  cofonr  8695  naddcllem  8697  naddov2  8700  naddunif  8714  naddasslem1  8715  naddasslem2  8716  ordtypelem2  9542  cantnfcl  9690  cantnflt  9695  cantnfp1lem3  9703  oemapvali  9707  cantnflem1c  9710  cantnflem1d  9711  cantnflem1  9712  cantnf  9716  cnfcom  9723  cnfcom3lem  9726  infxpenlem  10036  ac10ct  10057  dfac12lem1  10167  dfac12lem2  10168  cfeq0  10279  cfsuc  10280  cff1  10281  cfflb  10282  cofsmo  10292  cfsmolem  10293  alephsing  10299  zorn2lem2  10520  ttukeylem3  10534  ttukeylem5  10536  ttukeylem6  10537  inar1  10798  nosupno  27703  elold  27863  madefi  27905  oldfi  27906  ontgval  36373  aomclem6  43016  tfsconcatlem  43294  tfsconcatfv  43299  ofoafo  43314  ofoaid1  43316  ofoaid2  43317  dfno2  43386