Theorem onelss 5683

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

Syntax hints:   → wi 4   ∈ wcel 1977   ⊆ wss 3540  Ord word 5639  Oncon0 5640

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-rex 2902  df-v 3175  df-in 3547  df-ss 3554  df-uni 4373  df-tr 4681  df-po 4959  df-so 4960  df-fr 4997  df-we 4999  df-ord 5643  df-on 5644

This theorem is referenced by:  ordunidif  5690  onelssi  5753  ssorduni  6877  suceloni  6905  tfisi  6950  tfrlem9  7368  tfrlem11  7371  oaordex  7525  oaass  7528  odi  7546  omass  7547  oewordri  7559  nnaordex  7605  domtriord  7991  hartogs  8332  card2on  8342  tskwe  8659  infxpenlem  8719  cfub  8954  cfsuc  8962  coflim  8966  hsmexlem2  9132  ondomon  9264  pwcfsdom  9284  inar1  9476  tskord  9481  grudomon  9518  gruina  9519  dfrdg2  30945  poseq  30994  sltres  31061  nobndup  31099  nobnddown  31100  aomclem6  36647