Theorem ordelss 6175

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 6173	. 2 ⊢ (Ord 𝐴 → Tr 𝐴)
2		trss 5145	. . 3 ⊢ (Tr 𝐴 → (𝐵 ∈ 𝐴 → 𝐵 ⊆ 𝐴))
3	2	imp 410	. 2 ⊢ ((Tr 𝐴 ∧ 𝐵 ∈ 𝐴) → 𝐵 ⊆ 𝐴)
4	1, 3	sylan 583	1 ⊢ ((Ord 𝐴 ∧ 𝐵 ∈ 𝐴) → 𝐵 ⊆ 𝐴)

Syntax hints:   → wi 4   ∧ wa 399   ∈ wcel 2111   ⊆ wss 3881  Tr wtr 5136  Ord word 6158

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-11 2158  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-ral 3111  df-v 3443  df-in 3888  df-ss 3898  df-uni 4801  df-tr 5137  df-ord 6162

This theorem is referenced by:  onfr  6198  onelss  6201  ordtri2or2  6255  onfununi  7961  smores3  7973  tfrlem1  7995  tfrlem9a  8005  tz7.44-2  8026  tz7.44-3  8027  oaabslem  8253  oaabs2  8255  omabslem  8256  omabs  8257  findcard3  8745  nnsdomg  8761  ordiso2  8963  ordtypelem2  8967  ordtypelem6  8971  ordtypelem7  8972  cantnf  9140  cnfcomlem  9146  cardmin2  9412  infxpenlem  9424  iunfictbso  9525  dfac12lem2  9555  dfac12lem3  9556  unctb  9616  ackbij2lem1  9630  ackbij1lem3  9633  ackbij1lem18  9648  ackbij2  9654  ttukeylem6  9925  ttukeylem7  9926  alephexp1  9990  fpwwe2lem8  10048  pwfseqlem3  10071  pwdjundom  10078  fz1isolem  13815  onsuct0  33902  finxpreclem4  34811  grur1cld  40940