Theorem onelss 6403

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2142   ⊆ wss 3904  Ord word 6359  Oncon0 6360

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 401  df-tru 1572  df-ex 1809  df-sb 2096  df-clab 2741  df-cleq 2754  df-clel 2837  df-ral 3079  df-v 3456  df-ss 3921  df-uni 4872  df-tr 5218  df-po 5568  df-so 5569  df-fr 5613  df-we 5615  df-ord 6363  df-on 6364

This theorem is used by:  ordunidif  6411  onelssi  6477  ssorduni  7776  tfisi  7853  poseq  8152  tfrlem9  8370  tfrlem11  8373  oaordex  8541  oaass  8544  odi  8562  omass  8563  oewordri  8576  nnaordex  8622  domtriord  9109  hartogs  9504  card2on  9514  tskwe  9943  infxpenlem  10004  cfub  10238  cfsuc  10247  coflim  10251  hsmexlem2  10417  ondomon  10553  pwcfsdom  10574  inar1  10766  tskord  10771  grudomon  10808  gruina  10809  ltsres  27837  nosupno  27878  nosupbday  27880  noinfno  27893  oldssmade  28071  madebday  28104  mulsproplem13  28332  mulsproplem14  28333  dfrdg2  36293  onelssd  36701  aomclem6  43814  nnoeomeqom  44067  naddgeoa  44149  naddwordnexlem1  44152  naddwordnexlem4  44156  iscard5  44290