Theorem ordelss 6411

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2108   ⊆ wss 3976  Tr wtr 5283  Ord word 6394

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ral 3068  df-v 3490  df-ss 3993  df-uni 4932  df-tr 5284  df-ord 6398

This theorem is referenced by:  onfr  6434  onelss  6437  ordtri2or2  6494  onfununi  8397  smores3  8409  tfrlem1  8432  tfrlem9a  8442  tz7.44-2  8463  tz7.44-3  8464  oaabslem  8703  oaabs2  8705  omabslem  8706  omabs  8707  findcard3  9346  findcard3OLD  9347  nnsdomg  9363  nnsdomgOLD  9364  ordiso2  9584  ordtypelem2  9588  ordtypelem6  9592  ordtypelem7  9593  cantnf  9762  cnfcomlem  9768  ttrcltr  9785  cardmin2  10068  infxpenlem  10082  iunfictbso  10183  dfac12lem2  10214  dfac12lem3  10215  unctb  10273  ackbij2lem1  10287  ackbij1lem3  10290  ackbij1lem18  10305  ackbij2  10311  ttukeylem6  10583  ttukeylem7  10584  alephexp1  10648  fpwwe2lem7  10706  pwfseqlem3  10729  pwdjundom  10736  fz1isolem  14510  noinfbday  27783  onsuct0  36407  finxpreclem4  37360  nadd2rabtr  43346  grur1cld  44201