Theorem ordelss 6333

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2113   ⊆ wss 3901  Tr wtr 5205  Ord word 6316

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-ral 3052  df-v 3442  df-ss 3918  df-uni 4864  df-tr 5206  df-ord 6320

This theorem is referenced by:  onfr  6356  onelss  6359  ordtri2or2  6418  onfununi  8273  smores3  8285  tfrlem1  8307  tfrlem9a  8317  tz7.44-2  8338  tz7.44-3  8339  oaabslem  8575  oaabs2  8577  omabslem  8578  omabs  8579  findcard3  9183  nnsdomg  9199  ordiso2  9420  ordtypelem2  9424  ordtypelem6  9428  ordtypelem7  9429  cantnf  9602  cnfcomlem  9608  ttrcltr  9625  cardmin2  9911  infxpenlem  9923  iunfictbso  10024  dfac12lem2  10055  dfac12lem3  10056  unctb  10114  ackbij2lem1  10128  ackbij1lem3  10131  ackbij1lem18  10146  ackbij2  10152  ttukeylem6  10424  ttukeylem7  10425  alephexp1  10490  fpwwe2lem7  10548  pwfseqlem3  10571  pwdjundom  10578  fz1isolem  14384  noinfbday  27688  onsuct0  36635  finxpreclem4  37599  nadd2rabtr  43626  grur1cld  44473