Theorem ordelss 5656

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 5654	. 2 ⊢ (Ord 𝐴 → Tr 𝐴)
2		trss 4689	. . 3 ⊢ (Tr 𝐴 → (𝐵 ∈ 𝐴 → 𝐵 ⊆ 𝐴))
3	2	imp 444	. 2 ⊢ ((Tr 𝐴 ∧ 𝐵 ∈ 𝐴) → 𝐵 ⊆ 𝐴)
4	1, 3	sylan 487	1 ⊢ ((Ord 𝐴 ∧ 𝐵 ∈ 𝐴) → 𝐵 ⊆ 𝐴)

Syntax hints:   → wi 4   ∧ wa 383   ∈ wcel 1977   ⊆ wss 3540  Tr wtr 4680  Ord word 5639

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-v 3175  df-in 3547  df-ss 3554  df-uni 4373  df-tr 4681  df-ord 5643

This theorem is referenced by:  onfr  5680  onelss  5683  ordtri2or2  5740  onfununi  7325  smores3  7337  tfrlem1  7359  tfrlem9a  7369  tz7.44-2  7390  tz7.44-3  7391  oaabslem  7610  oaabs2  7612  omabslem  7613  omabs  7614  findcard3  8088  nnsdomg  8104  ordiso2  8303  ordtypelem2  8307  ordtypelem6  8311  ordtypelem7  8312  cantnf  8473  cnfcomlem  8479  cardmin2  8707  infxpenlem  8719  iunfictbso  8820  dfac12lem2  8849  dfac12lem3  8850  unctb  8910  ackbij2lem1  8924  ackbij1lem3  8927  ackbij1lem18  8942  ackbij2  8948  ttukeylem6  9219  ttukeylem7  9220  alephexp1  9280  fpwwe2lem8  9338  pwfseqlem3  9361  pwcdandom  9368  fz1isolem  13102  onsuct0  31610  finxpreclem4  32407