Theorem onss 7732

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

Syntax hints:   → wi 4   ∈ wcel 2114   ⊆ wss 3890  Ord word 6316  Oncon0 6317

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5231  ax-pr 5370

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-pss 3910  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-tr 5194  df-eprel 5524  df-po 5532  df-so 5533  df-fr 5577  df-we 5579  df-ord 6320  df-on 6321

This theorem is referenced by:  onuni  7735  onminex  7749  onssi  7782  tfi  7797  soseq  8102  tfr3  8331  tz7.49  8377  tz7.49c  8378  oacomf1olem  8492  oeeulem  8530  cofonr  8603  naddcllem  8605  naddov2  8608  naddunif  8622  naddasslem1  8623  naddasslem2  8624  ordtypelem2  9427  cantnfcl  9579  cantnflt  9584  cantnfp1lem3  9592  oemapvali  9596  cantnflem1c  9599  cantnflem1d  9600  cantnflem1  9601  cantnf  9605  cnfcom  9612  cnfcom3lem  9615  infxpenlem  9926  ac10ct  9947  dfac12lem1  10057  dfac12lem2  10058  cfeq0  10169  cfsuc  10170  cff1  10171  cfflb  10172  cofsmo  10182  cfsmolem  10183  alephsing  10189  zorn2lem2  10410  ttukeylem3  10424  ttukeylem5  10426  ttukeylem6  10427  inar1  10689  nosupno  27681  elold  27865  madefi  27919  oldfi  27920  oldfib  28383  ontgval  36629  aomclem6  43505  tfsconcatlem  43782  tfsconcatfv  43787  ofoafo  43802  ofoaid1  43804  ofoaid2  43805  dfno2  43873