Theorem ordelss 6368

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2108   ⊆ wss 3926  Tr wtr 5229  Ord word 6351

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-ral 3052  df-v 3461  df-ss 3943  df-uni 4884  df-tr 5230  df-ord 6355

This theorem is referenced by:  onfr  6391  onelss  6394  ordtri2or2  6453  onfununi  8355  smores3  8367  tfrlem1  8390  tfrlem9a  8400  tz7.44-2  8421  tz7.44-3  8422  oaabslem  8659  oaabs2  8661  omabslem  8662  omabs  8663  findcard3  9290  findcard3OLD  9291  nnsdomg  9307  nnsdomgOLD  9308  ordiso2  9529  ordtypelem2  9533  ordtypelem6  9537  ordtypelem7  9538  cantnf  9707  cnfcomlem  9713  ttrcltr  9730  cardmin2  10013  infxpenlem  10027  iunfictbso  10128  dfac12lem2  10159  dfac12lem3  10160  unctb  10218  ackbij2lem1  10232  ackbij1lem3  10235  ackbij1lem18  10250  ackbij2  10256  ttukeylem6  10528  ttukeylem7  10529  alephexp1  10593  fpwwe2lem7  10651  pwfseqlem3  10674  pwdjundom  10681  fz1isolem  14479  noinfbday  27684  onsuct0  36459  finxpreclem4  37412  nadd2rabtr  43408  grur1cld  44256