Theorem ordelss 6336

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109   ⊆ wss 3911  Tr wtr 5209  Ord word 6319

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-v 3446  df-ss 3928  df-uni 4868  df-tr 5210  df-ord 6323

This theorem is referenced by:  onfr  6359  onelss  6362  ordtri2or2  6421  onfununi  8287  smores3  8299  tfrlem1  8321  tfrlem9a  8331  tz7.44-2  8352  tz7.44-3  8353  oaabslem  8588  oaabs2  8590  omabslem  8591  omabs  8592  findcard3  9205  findcard3OLD  9206  nnsdomg  9222  nnsdomgOLD  9223  ordiso2  9444  ordtypelem2  9448  ordtypelem6  9452  ordtypelem7  9453  cantnf  9622  cnfcomlem  9628  ttrcltr  9645  cardmin2  9928  infxpenlem  9942  iunfictbso  10043  dfac12lem2  10074  dfac12lem3  10075  unctb  10133  ackbij2lem1  10147  ackbij1lem3  10150  ackbij1lem18  10165  ackbij2  10171  ttukeylem6  10443  ttukeylem7  10444  alephexp1  10508  fpwwe2lem7  10566  pwfseqlem3  10589  pwdjundom  10596  fz1isolem  14402  noinfbday  27608  onsuct0  36402  finxpreclem4  37355  nadd2rabtr  43346  grur1cld  44194