Theorem onelss 6377

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

Syntax hints:   → wi 4   ∈ wcel 2109   ⊆ wss 3917  Ord word 6334  Oncon0 6335

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 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-ral 3046  df-v 3452  df-ss 3934  df-uni 4875  df-tr 5218  df-po 5549  df-so 5550  df-fr 5594  df-we 5596  df-ord 6338  df-on 6339

This theorem is referenced by:  ordunidif  6385  onelssi  6452  ssorduni  7758  sucexeloniOLD  7789  tfisi  7838  poseq  8140  tfrlem9  8356  tfrlem11  8359  oaordex  8525  oaass  8528  odi  8546  omass  8547  oewordri  8559  nnaordex  8605  domtriord  9093  hartogs  9504  card2on  9514  tskwe  9910  infxpenlem  9973  cfub  10209  cfsuc  10217  coflim  10221  hsmexlem2  10387  ondomon  10523  pwcfsdom  10543  inar1  10735  tskord  10740  grudomon  10777  gruina  10778  sltres  27581  nosupno  27622  nosupbday  27624  noinfno  27637  oldssmade  27796  madebday  27818  mulsproplem13  28038  mulsproplem14  28039  dfrdg2  35790  aomclem6  43055  nnoeomeqom  43308  naddgeoa  43390  naddwordnexlem1  43393  naddwordnexlem4  43397  iscard5  43532