Theorem ordelss 6380

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

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2106   ⊆ wss 3948  Tr wtr 5265  Ord word 6363

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-ral 3062  df-v 3476  df-in 3955  df-ss 3965  df-uni 4909  df-tr 5266  df-ord 6367

This theorem is referenced by:  onfr  6403  onelss  6406  ordtri2or2  6463  onfununi  8340  smores3  8352  tfrlem1  8375  tfrlem9a  8385  tz7.44-2  8406  tz7.44-3  8407  oaabslem  8645  oaabs2  8647  omabslem  8648  omabs  8649  findcard3  9284  findcard3OLD  9285  nnsdomg  9301  nnsdomgOLD  9302  ordiso2  9509  ordtypelem2  9513  ordtypelem6  9517  ordtypelem7  9518  cantnf  9687  cnfcomlem  9693  ttrcltr  9710  cardmin2  9993  infxpenlem  10007  iunfictbso  10108  dfac12lem2  10138  dfac12lem3  10139  unctb  10199  ackbij2lem1  10213  ackbij1lem3  10216  ackbij1lem18  10231  ackbij2  10237  ttukeylem6  10508  ttukeylem7  10509  alephexp1  10573  fpwwe2lem7  10631  pwfseqlem3  10654  pwdjundom  10661  fz1isolem  14421  noinfbday  27220  onsuct0  35321  finxpreclem4  36270  nadd2rabtr  42124  grur1cld  42981