Theorem onelss 6359

Description: An element of an ordinal number is a subset of the number. (Contributed by NM, 5-Jun-1994.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)

Assertion

Ref	Expression
onelss	⊢ (𝐴 ∈ On → (𝐵 ∈ 𝐴 → 𝐵 ⊆ 𝐴))

Proof of Theorem onelss

Step	Hyp	Ref	Expression
1		eloni 6327	. 2 ⊢ (𝐴 ∈ On → Ord 𝐴)
2		ordelss 6333	. . 3 ⊢ ((Ord 𝐴 ∧ 𝐵 ∈ 𝐴) → 𝐵 ⊆ 𝐴)
3	2	ex 413	. 2 ⊢ (Ord 𝐴 → (𝐵 ∈ 𝐴 → 𝐵 ⊆ 𝐴))
4	1, 3	syl 17	1 ⊢ (𝐴 ∈ On → (𝐵 ∈ 𝐴 → 𝐵 ⊆ 𝐴))

Syntax hints:   → wi 4   ∈ wcel 2119   ⊆ 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 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-ral 3055  df-v 3434  df-ss 3907  df-uni 4846  df-tr 5187  df-po 5533  df-so 5534  df-fr 5578  df-we 5580  df-ord 6320  df-on 6321

This theorem is referenced by:  ordunidif  6367  onelssi  6433  ssorduni  7729  tfisi  7806  poseq  8105  tfrlem9  8321  tfrlem11  8324  oaordex  8490  oaass  8493  odi  8511  omass  8512  oewordri  8525  nnaordex  8571  domtriord  9058  hartogs  9456  card2on  9466  tskwe  9872  infxpenlem  9933  cfub  10169  cfsuc  10177  coflim  10181  hsmexlem2  10347  ondomon  10483  pwcfsdom  10504  inar1  10696  tskord  10701  grudomon  10738  gruina  10739  ltsres  27651  nosupno  27692  nosupbday  27694  noinfno  27707  oldssmade  27884  madebday  27917  mulsproplem13  28145  mulsproplem14  28146  dfrdg2  36022  aomclem6  43505  nnoeomeqom  43758  naddgeoa  43840  naddwordnexlem1  43843  naddwordnexlem4  43847  iscard5  43981