Theorem ordelss 6362

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 6360	. 2 ⊢ (Ord 𝐴 → Tr 𝐴)
2		trss 5217	. . 3 ⊢ (Tr 𝐴 → (𝐵 ∈ 𝐴 → 𝐵 ⊆ 𝐴))
3	2	imp 410	. 2 ⊢ ((Tr 𝐴 ∧ 𝐵 ∈ 𝐴) → 𝐵 ⊆ 𝐴)
4	1, 3	sylan 589	1 ⊢ ((Ord 𝐴 ∧ 𝐵 ∈ 𝐴) → 𝐵 ⊆ 𝐴)

Syntax hints:   → wi 4   ∧ wa 399   ∈ wcel 2142   ⊆ wss 3904  Tr wtr 5207  Ord word 6345

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1563  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-ral 3077  df-v 3456  df-ss 3921  df-uni 4866  df-tr 5208  df-ord 6349

This theorem is referenced by:  onfr  6385  onelss  6388  ordtri2or2  6447  onfununi  8312  smores3  8324  tfrlem1  8346  tfrlem9a  8357  tz7.44-2  8378  tz7.44-3  8379  oaabslem  8617  oaabs2  8619  omabslem  8620  omabs  8621  findcard3  9227  nnsdomg  9243  ordiso2  9463  ordtypelem2  9467  ordtypelem6  9471  ordtypelem7  9472  cantnf  9648  cnfcomlem  9654  ttrcltr  9671  cardmin2  9957  infxpenlem  9969  iunfictbso  10070  dfac12lem2  10101  dfac12lem3  10102  unctb  10160  ackbij2lem1  10174  ackbij1lem3  10177  ackbij1lem18  10192  ackbij2  10198  ttukeylem6  10471  ttukeylem7  10472  alephexp1  10537  fpwwe2lem7  10595  pwfseqlem3  10618  pwdjundom  10625  fz1isolem  14474  noinfbday  27784  onsuct0  36801  finxpreclem4  37888  nadd2rabtr  43961  grur1cld  44808