Theorem ordelss 6282

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

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2106   ⊆ wss 3887  Tr wtr 5191  Ord word 6265

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-11 2154  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-ral 3069  df-v 3434  df-in 3894  df-ss 3904  df-uni 4840  df-tr 5192  df-ord 6269

This theorem is referenced by:  onfr  6305  onelss  6308  ordtri2or2  6362  onfununi  8172  smores3  8184  tfrlem1  8207  tfrlem9a  8217  tz7.44-2  8238  tz7.44-3  8239  oaabslem  8477  oaabs2  8479  omabslem  8480  omabs  8481  findcard3  9057  nnsdomg  9073  ordiso2  9274  ordtypelem2  9278  ordtypelem6  9282  ordtypelem7  9283  cantnf  9451  cnfcomlem  9457  ttrcltr  9474  cardmin2  9757  infxpenlem  9769  iunfictbso  9870  dfac12lem2  9900  dfac12lem3  9901  unctb  9961  ackbij2lem1  9975  ackbij1lem3  9978  ackbij1lem18  9993  ackbij2  9999  ttukeylem6  10270  ttukeylem7  10271  alephexp1  10335  fpwwe2lem7  10393  pwfseqlem3  10416  pwdjundom  10423  fz1isolem  14175  noinfbday  33923  onsuct0  34630  finxpreclem4  35565  grur1cld  41850