Theorem onelss 6407

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

Syntax hints:   → wi 4   ∈ wcel 2107   ⊆ wss 3949  Ord word 6364  Oncon0 6365

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 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ral 3063  df-v 3477  df-in 3956  df-ss 3966  df-uni 4910  df-tr 5267  df-po 5589  df-so 5590  df-fr 5632  df-we 5634  df-ord 6368  df-on 6369

This theorem is referenced by:  ordunidif  6414  onelssi  6480  ssorduni  7766  sucexeloniOLD  7798  suceloniOLD  7800  tfisi  7848  poseq  8144  tfrlem9  8385  tfrlem11  8388  oaordex  8558  oaass  8561  odi  8579  omass  8580  oewordri  8592  nnaordex  8638  domtriord  9123  hartogs  9539  card2on  9549  tskwe  9945  infxpenlem  10008  cfub  10244  cfsuc  10252  coflim  10256  hsmexlem2  10422  ondomon  10558  pwcfsdom  10578  inar1  10770  tskord  10775  grudomon  10812  gruina  10813  sltres  27165  nosupno  27206  nosupbday  27208  noinfno  27221  oldssmade  27372  madebday  27394  mulsproplem13  27584  mulsproplem14  27585  dfrdg2  34767  aomclem6  41801  nnoeomeqom  42062  naddgeoa  42145  naddwordnexlem1  42148  naddwordnexlem4  42152  iscard5  42287