Theorem onelss 6308

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

Syntax hints:   → wi 4   ∈ wcel 2106   ⊆ wss 3887  Ord word 6265  Oncon0 6266

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-11 2154  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-ral 3069  df-v 3434  df-in 3894  df-ss 3904  df-uni 4840  df-tr 5192  df-po 5503  df-so 5504  df-fr 5544  df-we 5546  df-ord 6269  df-on 6270

This theorem is referenced by:  ordunidif  6314  onelssi  6375  ssorduni  7629  sucexeloni  7658  suceloniOLD  7660  tfisi  7705  tfrlem9  8216  tfrlem11  8219  oaordex  8389  oaass  8392  odi  8410  omass  8411  oewordri  8423  nnaordex  8469  domtriord  8910  hartogs  9303  card2on  9313  tskwe  9708  infxpenlem  9769  cfub  10005  cfsuc  10013  coflim  10017  hsmexlem2  10183  ondomon  10319  pwcfsdom  10339  inar1  10531  tskord  10536  grudomon  10573  gruina  10574  dfrdg2  33771  poseq  33802  sltres  33865  nosupno  33906  nosupbday  33908  noinfno  33921  oldssmade  34060  madebday  34080  aomclem6  40884  iscard5  41143