Theorem ordelss 6378

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 6376	. 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 6361

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 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-ral 3078  df-v 3453  df-ss 3916  df-uni 4868  df-tr 5213  df-ord 6365

This theorem is used by:  onfr  6402  onelss  6405  ordtri2or2  6464  onfununi  8349  smores3  8361  tfrlem1  8383  tfrlem9a  8394  tz7.44-2  8415  tz7.44-3  8416  oaabslem  8656  oaabs2  8658  omabslem  8659  omabs  8660  findcard3  9274  nnsdomg  9291  ordiso2  9509  ordtypelem2  9513  ordtypelem6  9517  ordtypelem7  9518  cantnf  9694  cnfcomlem  9700  ttrcltr  9717  cardmin2  10080  infxpenlem  10092  iunfictbso  10193  dfac12lem2  10223  dfac12lem3  10224  unctb  10282  ackbij2lem1  10296  ackbij1lem3  10299  ackbij1lem18  10314  ackbij2  10320  ttukeylem6  10592  ttukeylem7  10593  alephexp1  10664  fpwwe2lem7  10722  pwfseqlem3  10745  pwdjundom  10752  fz1isolem  14606  noinfbday  28077  onsuct0  37229  finxpreclem4  38317  nadd2rabtr  44385  grur1cld  45229