Theorem ordelss 6381

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 6379	. 2 ⊢ (Ord 𝐴 → Tr 𝐴)
2		trss 5221	. . 3 ⊢ (Tr 𝐴 → (𝐵 ∈ 𝐴 → 𝐵 ⊆ 𝐴))
3	2	imp 412	. 2 ⊢ ((Tr 𝐴 ∧ 𝐵 ∈ 𝐴) → 𝐵 ⊆ 𝐴)
4	1, 3	sylan 592	1 ⊢ ((Ord 𝐴 ∧ 𝐵 ∈ 𝐴) → 𝐵 ⊆ 𝐴)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2144   ⊆ wss 3896  Tr wtr 5211  Ord word 6364

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-v 3452  df-ss 3897  df-uni 4867  df-tr 5212  df-ord 6368

This theorem is used by:  onfr  6405  onelss  6408  ordtri2or2  6467  onfununi  8357  smores3  8369  tfrlem1  8391  tfrlem9a  8402  tz7.44-2  8423  tz7.44-3  8424  oaabslem  8664  oaabs2  8666  omabslem  8667  omabs  8668  findcard3  9282  nnsdomg  9299  ordiso2  9516  ordtypelem2  9520  ordtypelem6  9524  ordtypelem7  9525  cantnf  9701  cnfcomlem  9707  ttrcltr  9724  cardmin2  10087  infxpenlem  10099  iunfictbso  10200  dfac12lem2  10230  dfac12lem3  10231  unctb  10289  ackbij2lem1  10303  ackbij1lem3  10306  ackbij1lem18  10321  ackbij2  10327  ttukeylem6  10599  ttukeylem7  10600  alephexp1  10671  fpwwe2lem7  10729  pwfseqlem3  10752  pwdjundom  10759  fz1isolem  14613  noinfbday  28086  onsuct0  37353  finxpreclem4  38454  nadd2rabtr  44523  grur1cld  45367