Theorem ordelss 5992

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 5990	. 2 ⊢ (Ord 𝐴 → Tr 𝐴)
2		trss 4996	. . 3 ⊢ (Tr 𝐴 → (𝐵 ∈ 𝐴 → 𝐵 ⊆ 𝐴))
3	2	imp 397	. 2 ⊢ ((Tr 𝐴 ∧ 𝐵 ∈ 𝐴) → 𝐵 ⊆ 𝐴)
4	1, 3	sylan 575	1 ⊢ ((Ord 𝐴 ∧ 𝐵 ∈ 𝐴) → 𝐵 ⊆ 𝐴)

Syntax hints:   → wi 4   ∧ wa 386   ∈ wcel 2107   ⊆ wss 3792  Tr wtr 4987  Ord word 5975

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-ext 2754

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-ral 3095  df-v 3400  df-in 3799  df-ss 3806  df-uni 4672  df-tr 4988  df-ord 5979

This theorem is referenced by:  onfr  6015  onelss  6018  ordtri2or2  6072  onfununi  7721  smores3  7733  tfrlem1  7755  tfrlem9a  7765  tz7.44-2  7786  tz7.44-3  7787  oaabslem  8007  oaabs2  8009  omabslem  8010  omabs  8011  findcard3  8491  nnsdomg  8507  ordiso2  8709  ordtypelem2  8713  ordtypelem6  8717  ordtypelem7  8718  cantnf  8887  cnfcomlem  8893  cardmin2  9157  infxpenlem  9169  iunfictbso  9270  dfac12lem2  9301  dfac12lem3  9302  unctb  9362  ackbij2lem1  9376  ackbij1lem3  9379  ackbij1lem18  9394  ackbij2  9400  ttukeylem6  9671  ttukeylem7  9672  alephexp1  9736  fpwwe2lem8  9794  pwfseqlem3  9817  pwcdandom  9824  fz1isolem  13559  onsuct0  33023  finxpreclem4  33826