Theorem onelss 6404

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 6371	. 2 ⊢ (𝐴 ∈ On → Ord 𝐴)
2		ordelss 6377	. . 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 3902  Ord word 6360  Oncon0 6361

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 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-ral 3079  df-v 3455  df-ss 3919  df-uni 4871  df-tr 5217  df-po 5567  df-so 5568  df-fr 5612  df-we 5614  df-ord 6364  df-on 6365

This theorem is used by:  ordunidif  6412  onelssi  6478  ssorduni  7781  tfisi  7858  poseq  8159  tfrlem9  8377  tfrlem11  8380  oaordex  8548  oaass  8551  odi  8569  omass  8570  oewordri  8583  nnaordex  8629  domtriord  9124  hartogs  9519  card2on  9529  tskwe  9958  infxpenlem  10019  cfub  10253  cfsuc  10262  coflim  10266  hsmexlem2  10432  ondomon  10574  pwcfsdom  10595  inar1  10787  tskord  10792  grudomon  10829  gruina  10830  ltsres  27899  nosupno  27940  nosupbday  27942  noinfno  27955  oldssmade  28133  madebday  28166  mulsproplem13  28394  mulsproplem14  28395  dfrdg2  36374  onelssd  36783  aomclem6  43902  nnoeomeqom  44155  naddgeoa  44237  naddwordnexlem1  44240  naddwordnexlem4  44244  iscard5  44378