Theorem onelss 6392

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

Syntax hints:   → wi 4   ∈ wcel 2145   ⊆ wss 3907  Ord word 6349  Oncon0 6350

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1566  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-ral 3080  df-v 3459  df-ss 3924  df-uni 4869  df-tr 5213  df-po 5560  df-so 5561  df-fr 5605  df-we 5607  df-ord 6353  df-on 6354

This theorem is referenced by:  ordunidif  6400  onelssi  6466  ssorduni  7766  tfisi  7843  poseq  8142  tfrlem9  8360  tfrlem11  8363  oaordex  8531  oaass  8534  odi  8552  omass  8553  oewordri  8566  nnaordex  8612  domtriord  9099  hartogs  9494  card2on  9504  tskwe  9924  infxpenlem  9985  cfub  10220  cfsuc  10229  coflim  10233  hsmexlem2  10399  ondomon  10535  pwcfsdom  10556  inar1  10748  tskord  10753  grudomon  10790  gruina  10791  ltsres  27784  nosupno  27825  nosupbday  27827  noinfno  27840  oldssmade  28018  madebday  28051  mulsproplem13  28279  mulsproplem14  28280  dfrdg2  36156  aomclem6  43648  nnoeomeqom  43901  naddgeoa  43983  naddwordnexlem1  43986  naddwordnexlem4  43990  iscard5  44124