Theorem ordelss 6373

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 6371	. 2 ⊢ (Ord 𝐴 → Tr 𝐴)
2		trss 5222	. . 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 2145   ⊆ wss 3899  Tr wtr 5212  Ord word 6356

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-v 3452  df-ss 3916  df-uni 4868  df-tr 5213  df-ord 6360

This theorem is used by:  onfr  6397  onelss  6400  ordtri2or2  6459  onfununi  8331  smores3  8343  tfrlem1  8365  tfrlem9a  8376  tz7.44-2  8397  tz7.44-3  8398  oaabslem  8636  oaabs2  8638  omabslem  8639  omabs  8640  findcard3  9254  nnsdomg  9270  ordiso2  9488  ordtypelem2  9492  ordtypelem6  9496  ordtypelem7  9497  cantnf  9673  cnfcomlem  9679  ttrcltr  9696  cardmin2  10005  infxpenlem  10017  iunfictbso  10118  dfac12lem2  10148  dfac12lem3  10149  unctb  10207  ackbij2lem1  10221  ackbij1lem3  10224  ackbij1lem18  10239  ackbij2  10245  ttukeylem6  10517  ttukeylem7  10518  alephexp1  10589  fpwwe2lem7  10647  pwfseqlem3  10670  pwdjundom  10677  fz1isolem  14527  noinfbday  27957  onsuct0  37061  finxpreclem4  38149  nadd2rabtr  44226  grur1cld  45071