Theorem ordelss 6326

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 6324	. 2 ⊢ (Ord 𝐴 → Tr 𝐴)
2		trss 5189	. . 3 ⊢ (Tr 𝐴 → (𝐵 ∈ 𝐴 → 𝐵 ⊆ 𝐴))
3	2	imp 407	. 2 ⊢ ((Tr 𝐴 ∧ 𝐵 ∈ 𝐴) → 𝐵 ⊆ 𝐴)
4	1, 3	sylan 586	1 ⊢ ((Ord 𝐴 ∧ 𝐵 ∈ 𝐴) → 𝐵 ⊆ 𝐴)

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2119   ⊆ wss 3883  Tr wtr 5179  Ord word 6309

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-ral 3054  df-v 3433  df-ss 3900  df-uni 4839  df-tr 5180  df-ord 6313

This theorem is referenced by:  onfr  6349  onelss  6352  ordtri2or2  6411  onfununi  8271  smores3  8283  tfrlem1  8305  tfrlem9a  8315  tz7.44-2  8336  tz7.44-3  8337  oaabslem  8573  oaabs2  8575  omabslem  8576  omabs  8577  findcard3  9183  nnsdomg  9199  ordiso2  9420  ordtypelem2  9424  ordtypelem6  9428  ordtypelem7  9429  cantnf  9605  cnfcomlem  9611  ttrcltr  9628  cardmin2  9914  infxpenlem  9926  iunfictbso  10027  dfac12lem2  10058  dfac12lem3  10059  unctb  10117  ackbij2lem1  10131  ackbij1lem3  10134  ackbij1lem18  10149  ackbij2  10155  ttukeylem6  10427  ttukeylem7  10428  alephexp1  10493  fpwwe2lem7  10551  pwfseqlem3  10574  pwdjundom  10581  fz1isolem  14414  noinfbday  27702  onsuct0  36669  finxpreclem4  37756  nadd2rabtr  43829  grur1cld  44676