Theorem ordelss 6377

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 6375	. 2 ⊢ (Ord 𝐴 → Tr 𝐴)
2		trss 5232	. . 3 ⊢ (Tr 𝐴 → (𝐵 ∈ 𝐴 → 𝐵 ⊆ 𝐴))
3	2	imp 411	. 2 ⊢ ((Tr 𝐴 ∧ 𝐵 ∈ 𝐴) → 𝐵 ⊆ 𝐴)
4	1, 3	sylan 591	1 ⊢ ((Ord 𝐴 ∧ 𝐵 ∈ 𝐴) → 𝐵 ⊆ 𝐴)

Syntax hints:   → wi 4   ∧ wa 400   ∈ wcel 2149   ⊆ wss 3913  Tr wtr 5222  Ord word 6360

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-ral 3086  df-v 3465  df-ss 3930  df-uni 4877  df-tr 5223  df-ord 6364

This theorem is referenced by:  onfr  6401  onelss  6404  ordtri2or2  6463  onfununi  8328  smores3  8340  tfrlem1  8362  tfrlem9a  8373  tz7.44-2  8394  tz7.44-3  8395  oaabslem  8633  oaabs2  8635  omabslem  8636  omabs  8637  findcard3  9243  nnsdomg  9259  ordiso2  9477  ordtypelem2  9481  ordtypelem6  9485  ordtypelem7  9486  cantnf  9662  cnfcomlem  9668  ttrcltr  9685  cardmin2  9985  infxpenlem  9997  iunfictbso  10098  dfac12lem2  10128  dfac12lem3  10129  unctb  10187  ackbij2lem1  10201  ackbij1lem3  10204  ackbij1lem18  10219  ackbij2  10225  ttukeylem6  10498  ttukeylem7  10499  alephexp1  10564  fpwwe2lem7  10622  pwfseqlem3  10645  pwdjundom  10652  fz1isolem  14498  noinfbday  27850  onsuct0  36841  finxpreclem4  37928  nadd2rabtr  44003  grur1cld  44848