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 2144   ⊆ wss 3895  Ord word 6361  Oncon0 6362

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-v 3452  df-ss 3896  df-uni 4867  df-tr 5212  df-po 5558  df-so 5559  df-fr 5603  df-we 5605  df-ord 6365  df-on 6366

This theorem is used by:  ordunidif  6413  onelssi  6479  ssorduni  7793  tfisi  7870  poseq  8175  tfrlem9  8394  tfrlem11  8397  oaordex  8567  oaass  8570  odi  8588  omass  8589  oewordri  8602  nnaordex  8648  domtriord  9143  hartogs  9539  card2on  9549  tskwe  10032  infxpenlem  10093  cfub  10327  cfsuc  10336  coflim  10340  hsmexlem2  10506  ondomon  10648  pwcfsdom  10669  inar1  10861  tskord  10866  grudomon  10903  gruina  10904  ltsres  28020  nosupno  28061  nosupbday  28063  noinfno  28076  oldssmade  28254  madebday  28287  mulsproplem13  28515  mulsproplem14  28516  maxssj0  35938  dfrdg2  36632  onelssd  37025  aomclem6  44137  nnoeomeqom  44390  naddgeoa  44472  naddwordnexlem1  44475  naddwordnexlem4  44479  iscard5  44613