Theorem onelss 6374

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

Syntax hints:   → wi 4   ∈ wcel 2109   ⊆ wss 3914  Ord word 6331  Oncon0 6332

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 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-v 3449  df-ss 3931  df-uni 4872  df-tr 5215  df-po 5546  df-so 5547  df-fr 5591  df-we 5593  df-ord 6335  df-on 6336

This theorem is referenced by:  ordunidif  6382  onelssi  6449  ssorduni  7755  sucexeloniOLD  7786  tfisi  7835  poseq  8137  tfrlem9  8353  tfrlem11  8356  oaordex  8522  oaass  8525  odi  8543  omass  8544  oewordri  8556  nnaordex  8602  domtriord  9087  hartogs  9497  card2on  9507  tskwe  9903  infxpenlem  9966  cfub  10202  cfsuc  10210  coflim  10214  hsmexlem2  10380  ondomon  10516  pwcfsdom  10536  inar1  10728  tskord  10733  grudomon  10770  gruina  10771  sltres  27574  nosupno  27615  nosupbday  27617  noinfno  27630  oldssmade  27789  madebday  27811  mulsproplem13  28031  mulsproplem14  28032  dfrdg2  35783  aomclem6  43048  nnoeomeqom  43301  naddgeoa  43383  naddwordnexlem1  43386  naddwordnexlem4  43390  iscard5  43525