Theorem onelss 6233

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

Syntax hints:   → wi 4   ∈ wcel 2112   ⊆ wss 3853  Ord word 6190  Oncon0 6191

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-11 2160  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1546  df-ex 1788  df-sb 2073  df-clab 2715  df-cleq 2728  df-clel 2809  df-ral 3056  df-v 3400  df-in 3860  df-ss 3870  df-uni 4806  df-tr 5147  df-po 5453  df-so 5454  df-fr 5494  df-we 5496  df-ord 6194  df-on 6195

This theorem is referenced by:  ordunidif  6239  onelssi  6300  ssorduni  7541  suceloni  7570  tfisi  7615  tfrlem9  8099  tfrlem11  8102  oaordex  8264  oaass  8267  odi  8285  omass  8286  oewordri  8298  nnaordex  8344  domtriord  8770  hartogs  9138  card2on  9148  tskwe  9531  infxpenlem  9592  cfub  9828  cfsuc  9836  coflim  9840  hsmexlem2  10006  ondomon  10142  pwcfsdom  10162  inar1  10354  tskord  10359  grudomon  10396  gruina  10397  dfrdg2  33441  poseq  33482  sltres  33551  nosupno  33592  nosupbday  33594  noinfno  33607  oldssmade  33746  madebday  33766  aomclem6  40528  iscard5  40767