Theorem onelss 6394

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 6361	. 2 ⊢ (𝐴 ∈ On → Ord 𝐴)
2		ordelss 6367	. . 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 3898  Ord word 6350  Oncon0 6351

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 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-v 3452  df-ss 3915  df-uni 4867  df-tr 5212  df-po 5555  df-so 5556  df-fr 5600  df-we 5602  df-ord 6354  df-on 6355

This theorem is used by:  ordunidif  6402  onelssi  6468  ssorduni  7776  tfisi  7853  poseq  8153  tfrlem9  8371  tfrlem11  8374  oaordex  8544  oaass  8547  odi  8565  omass  8566  oewordri  8579  nnaordex  8625  domtriord  9120  hartogs  9516  card2on  9526  tskwe  10003  infxpenlem  10064  cfub  10298  cfsuc  10307  coflim  10311  hsmexlem2  10477  ondomon  10619  pwcfsdom  10640  inar1  10832  tskord  10837  grudomon  10874  gruina  10875  ltsres  27953  nosupno  27994  nosupbday  27996  noinfno  28009  oldssmade  28187  madebday  28220  mulsproplem13  28448  mulsproplem14  28449  dfrdg2  36479  onelssd  36872  aomclem6  44004  nnoeomeqom  44257  naddgeoa  44339  naddwordnexlem1  44342  naddwordnexlem4  44346  iscard5  44480