Theorem ordelss 6376

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

Syntax hints:   → wi 4   ∧ wa 400   ∈ wcel 2143   ⊆ wss 3905  Tr wtr 5218  Ord word 6359

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ral 3080  df-v 3457  df-ss 3922  df-uni 4873  df-tr 5219  df-ord 6363

This theorem is referenced by:  onfr  6400  onelss  6403  ordtri2or2  6462  onfununi  8324  smores3  8336  tfrlem1  8358  tfrlem9a  8369  tz7.44-2  8390  tz7.44-3  8391  oaabslem  8629  oaabs2  8631  omabslem  8632  omabs  8633  findcard3  9239  nnsdomg  9255  ordiso2  9473  ordtypelem2  9477  ordtypelem6  9481  ordtypelem7  9482  cantnf  9658  cnfcomlem  9664  ttrcltr  9681  cardmin2  9981  infxpenlem  9993  iunfictbso  10094  dfac12lem2  10124  dfac12lem3  10125  unctb  10183  ackbij2lem1  10197  ackbij1lem3  10200  ackbij1lem18  10215  ackbij2  10221  ttukeylem6  10493  ttukeylem7  10494  alephexp1  10559  fpwwe2lem7  10617  pwfseqlem3  10640  pwdjundom  10647  fz1isolem  14494  noinfbday  27884  onsuct0  36952  finxpreclem4  38040  nadd2rabtr  44111  grur1cld  44956