Theorem onelss 6405

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

Syntax hints:   → wi 4   ∈ wcel 2107   ⊆ wss 3931  Ord word 6362  Oncon0 6363

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1542  df-ex 1779  df-sb 2064  df-clab 2713  df-cleq 2726  df-clel 2808  df-ral 3051  df-v 3465  df-ss 3948  df-uni 4888  df-tr 5240  df-po 5572  df-so 5573  df-fr 5617  df-we 5619  df-ord 6366  df-on 6367

This theorem is referenced by:  ordunidif  6413  onelssi  6479  ssorduni  7781  sucexeloniOLD  7812  suceloniOLD  7814  tfisi  7862  poseq  8165  tfrlem9  8407  tfrlem11  8410  oaordex  8578  oaass  8581  odi  8599  omass  8600  oewordri  8612  nnaordex  8658  domtriord  9145  hartogs  9566  card2on  9576  tskwe  9972  infxpenlem  10035  cfub  10271  cfsuc  10279  coflim  10283  hsmexlem2  10449  ondomon  10585  pwcfsdom  10605  inar1  10797  tskord  10802  grudomon  10839  gruina  10840  sltres  27643  nosupno  27684  nosupbday  27686  noinfno  27699  oldssmade  27852  madebday  27874  mulsproplem13  28090  mulsproplem14  28091  dfrdg2  35755  aomclem6  43034  nnoeomeqom  43287  naddgeoa  43369  naddwordnexlem1  43372  naddwordnexlem4  43376  iscard5  43511