Theorem onelss 6108

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 6076	. 2 ⊢ (𝐴 ∈ On → Ord 𝐴)
2		ordelss 6082	. . 3 ⊢ ((Ord 𝐴 ∧ 𝐵 ∈ 𝐴) → 𝐵 ⊆ 𝐴)
3	2	ex 413	. 2 ⊢ (Ord 𝐴 → (𝐵 ∈ 𝐴 → 𝐵 ⊆ 𝐴))
4	1, 3	syl 17	1 ⊢ (𝐴 ∈ On → (𝐵 ∈ 𝐴 → 𝐵 ⊆ 𝐴))

Syntax hints:   → wi 4   ∈ wcel 2081   ⊆ wss 3859  Ord word 6065  Oncon0 6066

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-ext 2769

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-ral 3110  df-rex 3111  df-v 3439  df-in 3866  df-ss 3874  df-uni 4746  df-tr 5064  df-po 5362  df-so 5363  df-fr 5402  df-we 5404  df-ord 6069  df-on 6070

This theorem is referenced by:  ordunidif  6114  onelssi  6174  ssorduni  7356  suceloni  7384  tfisi  7429  tfrlem9  7873  tfrlem11  7876  oaordex  8034  oaass  8037  odi  8055  omass  8056  oewordri  8068  nnaordex  8114  domtriord  8510  hartogs  8854  card2on  8864  tskwe  9225  infxpenlem  9285  cfub  9517  cfsuc  9525  coflim  9529  hsmexlem2  9695  ondomon  9831  pwcfsdom  9851  inar1  10043  tskord  10048  grudomon  10085  gruina  10086  dfrdg2  32650  poseq  32705  sltres  32779  nosupno  32813  aomclem6  39163  iscard5  39405