Theorem ordelss 6387

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 6385	. 2 ⊢ (Ord 𝐴 → Tr 𝐴)
2		trss 5277	. . 3 ⊢ (Tr 𝐴 → (𝐵 ∈ 𝐴 → 𝐵 ⊆ 𝐴))
3	2	imp 405	. 2 ⊢ ((Tr 𝐴 ∧ 𝐵 ∈ 𝐴) → 𝐵 ⊆ 𝐴)
4	1, 3	sylan 578	1 ⊢ ((Ord 𝐴 ∧ 𝐵 ∈ 𝐴) → 𝐵 ⊆ 𝐴)

Syntax hints:   → wi 4   ∧ wa 394   ∈ wcel 2098   ⊆ wss 3944  Tr wtr 5266  Ord word 6370

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1536  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-ral 3051  df-v 3463  df-ss 3961  df-uni 4910  df-tr 5267  df-ord 6374

This theorem is referenced by:  onfr  6410  onelss  6413  ordtri2or2  6470  onfununi  8362  smores3  8374  tfrlem1  8397  tfrlem9a  8407  tz7.44-2  8428  tz7.44-3  8429  oaabslem  8668  oaabs2  8670  omabslem  8671  omabs  8672  findcard3  9310  findcard3OLD  9311  nnsdomg  9327  nnsdomgOLD  9328  ordiso2  9540  ordtypelem2  9544  ordtypelem6  9548  ordtypelem7  9549  cantnf  9718  cnfcomlem  9724  ttrcltr  9741  cardmin2  10024  infxpenlem  10038  iunfictbso  10139  dfac12lem2  10169  dfac12lem3  10170  unctb  10230  ackbij2lem1  10244  ackbij1lem3  10247  ackbij1lem18  10262  ackbij2  10268  ttukeylem6  10539  ttukeylem7  10540  alephexp1  10604  fpwwe2lem7  10662  pwfseqlem3  10685  pwdjundom  10692  fz1isolem  14458  noinfbday  27699  onsuct0  36056  finxpreclem4  37004  nadd2rabtr  42955  grur1cld  43811