Theorem onelss 6426

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

Syntax hints:   → wi 4   ∈ wcel 2108   ⊆ wss 3951  Ord word 6383  Oncon0 6384

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ral 3062  df-v 3482  df-ss 3968  df-uni 4908  df-tr 5260  df-po 5592  df-so 5593  df-fr 5637  df-we 5639  df-ord 6387  df-on 6388

This theorem is referenced by:  ordunidif  6433  onelssi  6499  ssorduni  7799  sucexeloniOLD  7830  suceloniOLD  7832  tfisi  7880  poseq  8183  tfrlem9  8425  tfrlem11  8428  oaordex  8596  oaass  8599  odi  8617  omass  8618  oewordri  8630  nnaordex  8676  domtriord  9163  hartogs  9584  card2on  9594  tskwe  9990  infxpenlem  10053  cfub  10289  cfsuc  10297  coflim  10301  hsmexlem2  10467  ondomon  10603  pwcfsdom  10623  inar1  10815  tskord  10820  grudomon  10857  gruina  10858  sltres  27707  nosupno  27748  nosupbday  27750  noinfno  27763  oldssmade  27916  madebday  27938  mulsproplem13  28154  mulsproplem14  28155  dfrdg2  35796  aomclem6  43071  nnoeomeqom  43325  naddgeoa  43407  naddwordnexlem1  43410  naddwordnexlem4  43414  iscard5  43549