Theorem onss 7780

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

Syntax hints:   → wi 4   ∈ wcel 2143   ⊆ wss 3905  Ord word 6359  Oncon0 6360

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-sep 5257  ax-pr 5404

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ne 2959  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-pss 3925  df-nul 4287  df-if 4488  df-pw 4564  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-br 5110  df-opab 5174  df-tr 5219  df-eprel 5561  df-po 5569  df-so 5570  df-fr 5614  df-we 5616  df-ord 6363  df-on 6364

This theorem is referenced by:  onuni  7783  onminex  7797  onssi  7830  tfi  7845  soseq  8151  tfr3  8382  tz7.49  8428  tz7.49c  8429  oacomf1olem  8545  oeeulem  8583  cofonr  8656  naddcllem  8658  naddov2  8661  naddunif  8676  naddasslem1  8677  naddasslem2  8678  ordtypelem2  9477  cantnfcl  9632  cantnflt  9637  cantnfp1lem3  9645  oemapvali  9649  cantnflem1c  9652  cantnflem1d  9653  cantnflem1  9654  cantnf  9658  cnfcom  9665  cnfcom3lem  9668  infxpenlem  9993  ac10ct  10014  dfac12lem1  10123  dfac12lem2  10124  cfeq0  10235  cfsuc  10236  cff1  10237  cfflb  10238  cofsmo  10248  cfsmolem  10249  alephsing  10255  zorn2lem2  10476  ttukeylem3  10490  ttukeylem5  10492  ttukeylem6  10493  inar1  10755  nosupno  27867  elold  28052  madefi  28106  oldfi  28107  oldfib  28570  ltnadd  36695  naddle  36696  nmulrid  36697  ontgval  36942  aomclem6  43786  tfsconcatlem  44063  tfsconcatfv  44068  ofoafo  44083  ofoaid1  44085  ofoaid2  44086  dfno2  44154