Theorem ordelss 6400

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 6398	. 2 ⊢ (Ord 𝐴 → Tr 𝐴)
2		trss 5270	. . 3 ⊢ (Tr 𝐴 → (𝐵 ∈ 𝐴 → 𝐵 ⊆ 𝐴))
3	2	imp 406	. 2 ⊢ ((Tr 𝐴 ∧ 𝐵 ∈ 𝐴) → 𝐵 ⊆ 𝐴)
4	1, 3	sylan 580	1 ⊢ ((Ord 𝐴 ∧ 𝐵 ∈ 𝐴) → 𝐵 ⊆ 𝐴)

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2108   ⊆ wss 3951  Tr wtr 5259  Ord word 6383

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ral 3062  df-v 3482  df-ss 3968  df-uni 4908  df-tr 5260  df-ord 6387

This theorem is referenced by:  onfr  6423  onelss  6426  ordtri2or2  6483  onfununi  8381  smores3  8393  tfrlem1  8416  tfrlem9a  8426  tz7.44-2  8447  tz7.44-3  8448  oaabslem  8685  oaabs2  8687  omabslem  8688  omabs  8689  findcard3  9318  findcard3OLD  9319  nnsdomg  9335  nnsdomgOLD  9336  ordiso2  9555  ordtypelem2  9559  ordtypelem6  9563  ordtypelem7  9564  cantnf  9733  cnfcomlem  9739  ttrcltr  9756  cardmin2  10039  infxpenlem  10053  iunfictbso  10154  dfac12lem2  10185  dfac12lem3  10186  unctb  10244  ackbij2lem1  10258  ackbij1lem3  10261  ackbij1lem18  10276  ackbij2  10282  ttukeylem6  10554  ttukeylem7  10555  alephexp1  10619  fpwwe2lem7  10677  pwfseqlem3  10700  pwdjundom  10707  fz1isolem  14500  noinfbday  27765  onsuct0  36442  finxpreclem4  37395  nadd2rabtr  43397  grur1cld  44251