Theorem ordelss 6380

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

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2106   ⊆ wss 3948  Tr wtr 5265  Ord word 6363

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-ral 3062  df-v 3476  df-in 3955  df-ss 3965  df-uni 4909  df-tr 5266  df-ord 6367

This theorem is referenced by:  onfr  6403  onelss  6406  ordtri2or2  6463  onfununi  8343  smores3  8355  tfrlem1  8378  tfrlem9a  8388  tz7.44-2  8409  tz7.44-3  8410  oaabslem  8648  oaabs2  8650  omabslem  8651  omabs  8652  findcard3  9287  findcard3OLD  9288  nnsdomg  9304  nnsdomgOLD  9305  ordiso2  9512  ordtypelem2  9516  ordtypelem6  9520  ordtypelem7  9521  cantnf  9690  cnfcomlem  9696  ttrcltr  9713  cardmin2  9996  infxpenlem  10010  iunfictbso  10111  dfac12lem2  10141  dfac12lem3  10142  unctb  10202  ackbij2lem1  10216  ackbij1lem3  10219  ackbij1lem18  10234  ackbij2  10240  ttukeylem6  10511  ttukeylem7  10512  alephexp1  10576  fpwwe2lem7  10634  pwfseqlem3  10657  pwdjundom  10664  fz1isolem  14426  noinfbday  27447  onsuct0  35629  finxpreclem4  36578  nadd2rabtr  42436  grur1cld  43293