Theorem ordelss 6323

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109   ⊆ wss 3903  Tr wtr 5199  Ord word 6306

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-v 3438  df-ss 3920  df-uni 4859  df-tr 5200  df-ord 6310

This theorem is referenced by:  onfr  6346  onelss  6349  ordtri2or2  6408  onfununi  8264  smores3  8276  tfrlem1  8298  tfrlem9a  8308  tz7.44-2  8329  tz7.44-3  8330  oaabslem  8565  oaabs2  8567  omabslem  8568  omabs  8569  findcard3  9172  nnsdomg  9188  ordiso2  9407  ordtypelem2  9411  ordtypelem6  9415  ordtypelem7  9416  cantnf  9589  cnfcomlem  9595  ttrcltr  9612  cardmin2  9895  infxpenlem  9907  iunfictbso  10008  dfac12lem2  10039  dfac12lem3  10040  unctb  10098  ackbij2lem1  10112  ackbij1lem3  10115  ackbij1lem18  10130  ackbij2  10136  ttukeylem6  10408  ttukeylem7  10409  alephexp1  10473  fpwwe2lem7  10531  pwfseqlem3  10554  pwdjundom  10561  fz1isolem  14368  noinfbday  27630  onsuct0  36415  finxpreclem4  37368  nadd2rabtr  43357  grur1cld  44205