Theorem ordelss 6380

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 6378	. 2 ⊢ (Ord 𝐴 → Tr 𝐴)
2		trss 5230	. . 3 ⊢ (Tr 𝐴 → (𝐵 ∈ 𝐴 → 𝐵 ⊆ 𝐴))
3	2	imp 412	. 2 ⊢ ((Tr 𝐴 ∧ 𝐵 ∈ 𝐴) → 𝐵 ⊆ 𝐴)
4	1, 3	sylan 592	1 ⊢ ((Ord 𝐴 ∧ 𝐵 ∈ 𝐴) → 𝐵 ⊆ 𝐴)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2146   ⊆ wss 3906  Tr wtr 5220  Ord word 6363

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-ral 3082  df-v 3459  df-ss 3923  df-uni 4875  df-tr 5221  df-ord 6367

This theorem is used by:  onfr  6404  onelss  6407  ordtri2or2  6466  onfununi  8334  smores3  8346  tfrlem1  8368  tfrlem9a  8379  tz7.44-2  8400  tz7.44-3  8401  oaabslem  8639  oaabs2  8641  omabslem  8642  omabs  8643  findcard3  9250  nnsdomg  9266  ordiso2  9484  ordtypelem2  9488  ordtypelem6  9492  ordtypelem7  9493  cantnf  9669  cnfcomlem  9675  ttrcltr  9692  cardmin2  10001  infxpenlem  10013  iunfictbso  10114  dfac12lem2  10144  dfac12lem3  10145  unctb  10203  ackbij2lem1  10217  ackbij1lem3  10220  ackbij1lem18  10235  ackbij2  10241  ttukeylem6  10513  ttukeylem7  10514  alephexp1  10579  fpwwe2lem7  10637  pwfseqlem3  10660  pwdjundom  10667  fz1isolem  14516  noinfbday  27935  onsuct0  37009  finxpreclem4  38097  nadd2rabtr  44169  grur1cld  45014