Theorem onelss 6356

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

Syntax hints:   → wi 4   ∈ wcel 2113   ⊆ wss 3899  Ord word 6313  Oncon0 6314

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-ral 3050  df-v 3440  df-ss 3916  df-uni 4861  df-tr 5203  df-po 5529  df-so 5530  df-fr 5574  df-we 5576  df-ord 6317  df-on 6318

This theorem is referenced by:  ordunidif  6364  onelssi  6430  ssorduni  7721  tfisi  7798  poseq  8097  tfrlem9  8313  tfrlem11  8316  oaordex  8482  oaass  8485  odi  8503  omass  8504  oewordri  8516  nnaordex  8562  domtriord  9046  hartogs  9440  card2on  9450  tskwe  9853  infxpenlem  9914  cfub  10150  cfsuc  10158  coflim  10162  hsmexlem2  10328  ondomon  10464  pwcfsdom  10484  inar1  10676  tskord  10681  grudomon  10718  gruina  10719  sltres  27611  nosupno  27652  nosupbday  27654  noinfno  27667  oldssmade  27832  madebday  27855  mulsproplem13  28077  mulsproplem14  28078  dfrdg2  35848  aomclem6  43166  nnoeomeqom  43419  naddgeoa  43501  naddwordnexlem1  43504  naddwordnexlem4  43508  iscard5  43643