Theorem onelss 6310

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

Syntax hints:   → wi 4   ∈ wcel 2106   ⊆ wss 3888  Ord word 6267  Oncon0 6268

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 3433  df-in 3895  df-ss 3905  df-uni 4842  df-tr 5194  df-po 5505  df-so 5506  df-fr 5546  df-we 5548  df-ord 6271  df-on 6272

This theorem is referenced by:  ordunidif  6316  onelssi  6377  ssorduni  7629  sucexeloni  7658  suceloniOLD  7660  tfisi  7705  tfrlem9  8214  tfrlem11  8217  oaordex  8387  oaass  8390  odi  8408  omass  8409  oewordri  8421  nnaordex  8467  domtriord  8908  hartogs  9301  card2on  9311  tskwe  9706  infxpenlem  9767  cfub  10003  cfsuc  10011  coflim  10015  hsmexlem2  10181  ondomon  10317  pwcfsdom  10337  inar1  10529  tskord  10534  grudomon  10571  gruina  10572  dfrdg2  33768  poseq  33799  sltres  33862  nosupno  33903  nosupbday  33905  noinfno  33918  oldssmade  34057  madebday  34077  aomclem6  40881  iscard5  41120