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 → (𝐵 ∈ 𝐴 → 𝐵 ⊆ 𝐴))

Syntax hints:   → wi 4   ∈ wcel 2141   ⊆ wss 3904  Ord word 6359  Oncon0 6360

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1571  df-ex 1808  df-sb 2095  df-clab 2740  df-cleq 2753  df-clel 2836  df-ral 3078  df-v 3455  df-ss 3921  df-uni 4872  df-tr 5218  df-po 5569  df-so 5570  df-fr 5614  df-we 5616  df-ord 6363  df-on 6364

This theorem is referenced by:  ordunidif  6411  onelssi  6477  ssorduni  7777  tfisi  7854  poseq  8153  tfrlem9  8371  tfrlem11  8374  oaordex  8542  oaass  8545  odi  8563  omass  8564  oewordri  8577  nnaordex  8623  domtriord  9110  hartogs  9505  card2on  9515  tskwe  9935  infxpenlem  9996  cfub  10231  cfsuc  10240  coflim  10244  hsmexlem2  10410  ondomon  10546  pwcfsdom  10567  inar1  10759  tskord  10764  grudomon  10801  gruina  10802  ltsres  27802  nosupno  27843  nosupbday  27845  noinfno  27858  oldssmade  28036  madebday  28069  mulsproplem13  28297  mulsproplem14  28298  dfrdg2  36251  aomclem6  43756  nnoeomeqom  44009  naddgeoa  44091  naddwordnexlem1  44094  naddwordnexlem4  44098  iscard5  44232