Theorem ordelss 6377

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 6375	. 2 ⊢ (Ord 𝐴 → Tr 𝐴)
2		trss 5232	. . 3 ⊢ (Tr 𝐴 → (𝐵 ∈ 𝐴 → 𝐵 ⊆ 𝐴))
3	2	imp 411	. 2 ⊢ ((Tr 𝐴 ∧ 𝐵 ∈ 𝐴) → 𝐵 ⊆ 𝐴)
4	1, 3	sylan 591	1 ⊢ ((Ord 𝐴 ∧ 𝐵 ∈ 𝐴) → 𝐵 ⊆ 𝐴)

Syntax hints:   → wi 4   ∧ wa 400   ∈ wcel 2149   ⊆ wss 3913  Tr wtr 5222  Ord word 6360

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-ral 3086  df-v 3465  df-ss 3930  df-uni 4877  df-tr 5223  df-ord 6364

This theorem is referenced by:  onfr  6401  onelss  6404  ordtri2or2  6463  onfununi  8327  smores3  8339  tfrlem1  8361  tfrlem9a  8372  tz7.44-2  8393  tz7.44-3  8394  oaabslem  8632  oaabs2  8634  omabslem  8635  omabs  8636  findcard3  9242  nnsdomg  9258  ordiso2  9476  ordtypelem2  9480  ordtypelem6  9484  ordtypelem7  9485  cantnf  9661  cnfcomlem  9667  ttrcltr  9684  cardmin2  9984  infxpenlem  9996  iunfictbso  10097  dfac12lem2  10127  dfac12lem3  10128  unctb  10186  ackbij2lem1  10200  ackbij1lem3  10203  ackbij1lem18  10218  ackbij2  10224  ttukeylem6  10497  ttukeylem7  10498  alephexp1  10563  fpwwe2lem7  10621  pwfseqlem3  10644  pwdjundom  10651  fz1isolem  14497  noinfbday  27849  onsuct0  36840  finxpreclem4  37927  nadd2rabtr  44002  grur1cld  44847