Theorem ordelss 5777

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

Syntax hints:   → wi 4   ∧ wa 383   ∈ wcel 2030   ⊆ wss 3607  Tr wtr 4785  Ord word 5760

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ral 2946  df-v 3233  df-in 3614  df-ss 3621  df-uni 4469  df-tr 4786  df-ord 5764

This theorem is referenced by:  onfr  5801  onelss  5804  ordtri2or2  5861  onfununi  7483  smores3  7495  tfrlem1  7517  tfrlem9a  7527  tz7.44-2  7548  tz7.44-3  7549  oaabslem  7768  oaabs2  7770  omabslem  7771  omabs  7772  findcard3  8244  nnsdomg  8260  ordiso2  8461  ordtypelem2  8465  ordtypelem6  8469  ordtypelem7  8470  cantnf  8628  cnfcomlem  8634  cardmin2  8862  infxpenlem  8874  iunfictbso  8975  dfac12lem2  9004  dfac12lem3  9005  unctb  9065  ackbij2lem1  9079  ackbij1lem3  9082  ackbij1lem18  9097  ackbij2  9103  ttukeylem6  9374  ttukeylem7  9375  alephexp1  9439  fpwwe2lem8  9497  pwfseqlem3  9520  pwcdandom  9527  fz1isolem  13283  onsuct0  32565  finxpreclem4  33361