Theorem onelss 6227

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

Syntax hints:   → wi 4   ∈ wcel 2110   ⊆ wss 3935  Ord word 6184  Oncon0 6185

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-rex 3144  df-v 3496  df-in 3942  df-ss 3951  df-uni 4832  df-tr 5165  df-po 5468  df-so 5469  df-fr 5508  df-we 5510  df-ord 6188  df-on 6189

This theorem is referenced by:  ordunidif  6233  onelssi  6293  ssorduni  7494  suceloni  7522  tfisi  7567  tfrlem9  8015  tfrlem11  8018  oaordex  8178  oaass  8181  odi  8199  omass  8200  oewordri  8212  nnaordex  8258  domtriord  8657  hartogs  9002  card2on  9012  tskwe  9373  infxpenlem  9433  cfub  9665  cfsuc  9673  coflim  9677  hsmexlem2  9843  ondomon  9979  pwcfsdom  9999  inar1  10191  tskord  10196  grudomon  10233  gruina  10234  dfrdg2  33035  poseq  33090  sltres  33164  nosupno  33198  aomclem6  39652  iscard5  39894