Theorem ordelss 6318

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2110   ⊆ wss 3900  Tr wtr 5196  Ord word 6301

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2112  ax-9 2120  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2722  df-clel 2804  df-ral 3046  df-v 3436  df-ss 3917  df-uni 4858  df-tr 5197  df-ord 6305

This theorem is referenced by:  onfr  6341  onelss  6344  ordtri2or2  6403  onfununi  8256  smores3  8268  tfrlem1  8290  tfrlem9a  8300  tz7.44-2  8321  tz7.44-3  8322  oaabslem  8557  oaabs2  8559  omabslem  8560  omabs  8561  findcard3  9162  nnsdomg  9178  ordiso2  9396  ordtypelem2  9400  ordtypelem6  9404  ordtypelem7  9405  cantnf  9578  cnfcomlem  9584  ttrcltr  9601  cardmin2  9884  infxpenlem  9896  iunfictbso  9997  dfac12lem2  10028  dfac12lem3  10029  unctb  10087  ackbij2lem1  10101  ackbij1lem3  10104  ackbij1lem18  10119  ackbij2  10125  ttukeylem6  10397  ttukeylem7  10398  alephexp1  10462  fpwwe2lem7  10520  pwfseqlem3  10543  pwdjundom  10550  fz1isolem  14360  noinfbday  27652  onsuct0  36454  finxpreclem4  37407  nadd2rabtr  43396  grur1cld  44244