Theorem ordelss 6331

Description: An element of an ordinal class is a subset of it. (Contributed by NM, 30-May-1994.)

Assertion

Ref	Expression
ordelss	⊢ ((Ord 𝐴 ∧ 𝐵 ∈ 𝐴) → 𝐵 ⊆ 𝐴)

Proof of Theorem ordelss

Step	Hyp	Ref	Expression
1		ordtr 6329	. 2 ⊢ (Ord 𝐴 → Tr 𝐴)
2		trss 5213	. . 3 ⊢ (Tr 𝐴 → (𝐵 ∈ 𝐴 → 𝐵 ⊆ 𝐴))
3	2	imp 406	. 2 ⊢ ((Tr 𝐴 ∧ 𝐵 ∈ 𝐴) → 𝐵 ⊆ 𝐴)
4	1, 3	sylan 580	1 ⊢ ((Ord 𝐴 ∧ 𝐵 ∈ 𝐴) → 𝐵 ⊆ 𝐴)

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2113   ⊆ wss 3899  Tr wtr 5203  Ord word 6314

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-ral 3050  df-v 3440  df-ss 3916  df-uni 4862  df-tr 5204  df-ord 6318

This theorem is referenced by:  onfr  6354  onelss  6357  ordtri2or2  6416  onfununi  8271  smores3  8283  tfrlem1  8305  tfrlem9a  8315  tz7.44-2  8336  tz7.44-3  8337  oaabslem  8573  oaabs2  8575  omabslem  8576  omabs  8577  findcard3  9181  nnsdomg  9197  ordiso2  9418  ordtypelem2  9422  ordtypelem6  9426  ordtypelem7  9427  cantnf  9600  cnfcomlem  9606  ttrcltr  9623  cardmin2  9909  infxpenlem  9921  iunfictbso  10022  dfac12lem2  10053  dfac12lem3  10054  unctb  10112  ackbij2lem1  10126  ackbij1lem3  10129  ackbij1lem18  10144  ackbij2  10150  ttukeylem6  10422  ttukeylem7  10423  alephexp1  10488  fpwwe2lem7  10546  pwfseqlem3  10569  pwdjundom  10576  fz1isolem  14382  noinfbday  27686  onsuct0  36584  finxpreclem4  37538  nadd2rabtr  43568  grur1cld  44415