Theorem ordelss 6279

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109   ⊆ wss 3891  Tr wtr 5195  Ord word 6262

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-11 2157  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1544  df-ex 1786  df-sb 2071  df-clab 2717  df-cleq 2731  df-clel 2817  df-ral 3070  df-v 3432  df-in 3898  df-ss 3908  df-uni 4845  df-tr 5196  df-ord 6266

This theorem is referenced by:  onfr  6302  onelss  6305  ordtri2or2  6359  onfununi  8156  smores3  8168  tfrlem1  8191  tfrlem9a  8201  tz7.44-2  8222  tz7.44-3  8223  oaabslem  8451  oaabs2  8453  omabslem  8454  omabs  8455  findcard3  9018  nnsdomg  9034  ordiso2  9235  ordtypelem2  9239  ordtypelem6  9243  ordtypelem7  9244  cantnf  9412  cnfcomlem  9418  ttrcltr  9435  cardmin2  9741  infxpenlem  9753  iunfictbso  9854  dfac12lem2  9884  dfac12lem3  9885  unctb  9945  ackbij2lem1  9959  ackbij1lem3  9962  ackbij1lem18  9977  ackbij2  9983  ttukeylem6  10254  ttukeylem7  10255  alephexp1  10319  fpwwe2lem7  10377  pwfseqlem3  10400  pwdjundom  10407  fz1isolem  14156  noinfbday  33902  onsuct0  34609  finxpreclem4  35544  grur1cld  41803