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 415	. 2 ⊢ (Ord 𝐴 → (𝐵 ∈ 𝐴 → 𝐵 ⊆ 𝐴))
4	1, 3	syl 17	1 ⊢ (𝐴 ∈ On → (𝐵 ∈ 𝐴 → 𝐵 ⊆ 𝐴))

Syntax hints:   → wi 4   ∈ wcel 2136   ⊆ wss 3899  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 1809  ax-4 1823  ax-5 1924  ax-6 1981  ax-7 2022  ax-8 2138  ax-9 2146  ax-ext 2728

This theorem depends on definitions:  df-bi 209  df-an 399  df-tru 1557  df-ex 1794  df-sb 2085  df-clab 2735  df-cleq 2748  df-clel 2831  df-ral 3071  df-v 3450  df-ss 3916  df-uni 4860  df-tr 5202  df-po 5548  df-so 5549  df-fr 5593  df-we 5595  df-ord 6338  df-on 6339

This theorem is referenced by:  ordunidif  6385  onelssi  6451  ssorduni  7751  tfisi  7828  poseq  8126  tfrlem9  8344  tfrlem11  8347  oaordex  8515  oaass  8518  odi  8536  omass  8537  oewordri  8550  nnaordex  8596  domtriord  9084  hartogs  9482  card2on  9492  tskwe  9898  infxpenlem  9959  cfub  10195  cfsuc  10204  coflim  10208  hsmexlem2  10374  ondomon  10510  pwcfsdom  10531  inar1  10723  tskord  10728  grudomon  10765  gruina  10766  ltsres  27696  nosupno  27737  nosupbday  27739  noinfno  27752  oldssmade  27930  madebday  27963  mulsproplem13  28191  mulsproplem14  28192  dfrdg2  36091  aomclem6  43584  nnoeomeqom  43837  naddgeoa  43919  naddwordnexlem1  43922  naddwordnexlem4  43926  iscard5  44060