Theorem ordelss 6381

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 6379	. 2 ⊢ (Ord 𝐴 → Tr 𝐴)
2		trss 5277	. . 3 ⊢ (Tr 𝐴 → (𝐵 ∈ 𝐴 → 𝐵 ⊆ 𝐴))
3	2	imp 408	. 2 ⊢ ((Tr 𝐴 ∧ 𝐵 ∈ 𝐴) → 𝐵 ⊆ 𝐴)
4	1, 3	sylan 581	1 ⊢ ((Ord 𝐴 ∧ 𝐵 ∈ 𝐴) → 𝐵 ⊆ 𝐴)

Syntax hints:   → wi 4   ∧ wa 397   ∈ wcel 2107   ⊆ wss 3949  Tr wtr 5266  Ord word 6364

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 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ral 3063  df-v 3477  df-in 3956  df-ss 3966  df-uni 4910  df-tr 5267  df-ord 6368

This theorem is referenced by:  onfr  6404  onelss  6407  ordtri2or2  6464  onfununi  8341  smores3  8353  tfrlem1  8376  tfrlem9a  8386  tz7.44-2  8407  tz7.44-3  8408  oaabslem  8646  oaabs2  8648  omabslem  8649  omabs  8650  findcard3  9285  findcard3OLD  9286  nnsdomg  9302  nnsdomgOLD  9303  ordiso2  9510  ordtypelem2  9514  ordtypelem6  9518  ordtypelem7  9519  cantnf  9688  cnfcomlem  9694  ttrcltr  9711  cardmin2  9994  infxpenlem  10008  iunfictbso  10109  dfac12lem2  10139  dfac12lem3  10140  unctb  10200  ackbij2lem1  10214  ackbij1lem3  10217  ackbij1lem18  10232  ackbij2  10238  ttukeylem6  10509  ttukeylem7  10510  alephexp1  10574  fpwwe2lem7  10632  pwfseqlem3  10655  pwdjundom  10662  fz1isolem  14422  noinfbday  27223  onsuct0  35326  finxpreclem4  36275  nadd2rabtr  42134  grur1cld  42991