Theorem ordelss 6351

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109   ⊆ wss 3917  Tr wtr 5217  Ord word 6334

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-ral 3046  df-v 3452  df-ss 3934  df-uni 4875  df-tr 5218  df-ord 6338

This theorem is referenced by:  onfr  6374  onelss  6377  ordtri2or2  6436  onfununi  8313  smores3  8325  tfrlem1  8347  tfrlem9a  8357  tz7.44-2  8378  tz7.44-3  8379  oaabslem  8614  oaabs2  8616  omabslem  8617  omabs  8618  findcard3  9236  findcard3OLD  9237  nnsdomg  9253  nnsdomgOLD  9254  ordiso2  9475  ordtypelem2  9479  ordtypelem6  9483  ordtypelem7  9484  cantnf  9653  cnfcomlem  9659  ttrcltr  9676  cardmin2  9959  infxpenlem  9973  iunfictbso  10074  dfac12lem2  10105  dfac12lem3  10106  unctb  10164  ackbij2lem1  10178  ackbij1lem3  10181  ackbij1lem18  10196  ackbij2  10202  ttukeylem6  10474  ttukeylem7  10475  alephexp1  10539  fpwwe2lem7  10597  pwfseqlem3  10620  pwdjundom  10627  fz1isolem  14433  noinfbday  27639  onsuct0  36436  finxpreclem4  37389  nadd2rabtr  43380  grur1cld  44228