Theorem onelss 6405

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 6372	. 2 ⊢ (𝐴 ∈ On → Ord 𝐴)
2		ordelss 6378	. . 3 ⊢ ((Ord 𝐴 ∧ 𝐵 ∈ 𝐴) → 𝐵 ⊆ 𝐴)
3	2	ex 418	. 2 ⊢ (Ord 𝐴 → (𝐵 ∈ 𝐴 → 𝐵 ⊆ 𝐴))
4	1, 3	syl 18	1 ⊢ (𝐴 ∈ On → (𝐵 ∈ 𝐴 → 𝐵 ⊆ 𝐴))

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145   ⊆ wss 3899  Ord word 6361  Oncon0 6362

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-ral 3078  df-v 3453  df-ss 3916  df-uni 4868  df-tr 5213  df-po 5559  df-so 5560  df-fr 5604  df-we 5606  df-ord 6365  df-on 6366

This theorem is used by:  ordunidif  6413  onelssi  6479  ssorduni  7793  tfisi  7870  poseq  8175  tfrlem9  8393  tfrlem11  8396  oaordex  8566  oaass  8569  odi  8587  omass  8588  oewordri  8601  nnaordex  8647  domtriord  9142  hartogs  9538  card2on  9548  tskwe  10031  infxpenlem  10092  cfub  10326  cfsuc  10335  coflim  10339  hsmexlem2  10505  ondomon  10647  pwcfsdom  10668  inar1  10860  tskord  10865  grudomon  10902  gruina  10903  ltsres  28019  nosupno  28060  nosupbday  28062  noinfno  28075  oldssmade  28253  madebday  28286  mulsproplem13  28514  mulsproplem14  28515  dfrdg2  36557  onelssd  36950  aomclem6  44061  nnoeomeqom  44314  naddgeoa  44396  naddwordnexlem1  44399  naddwordnexlem4  44403  iscard5  44537