Theorem ordelss 5893

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 5891	. 2 ⊢ (Ord 𝐴 → Tr 𝐴)
2		trss 4908	. . 3 ⊢ (Tr 𝐴 → (𝐵 ∈ 𝐴 → 𝐵 ⊆ 𝐴))
3	2	imp 394	. 2 ⊢ ((Tr 𝐴 ∧ 𝐵 ∈ 𝐴) → 𝐵 ⊆ 𝐴)
4	1, 3	sylan 570	1 ⊢ ((Ord 𝐴 ∧ 𝐵 ∈ 𝐴) → 𝐵 ⊆ 𝐴)

Syntax hints:   → wi 4   ∧ wa 383   ∈ wcel 2148   ⊆ wss 3729  Tr wtr 4899  Ord word 5876

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1873  ax-4 1888  ax-5 1994  ax-6 2060  ax-7 2096  ax-9 2157  ax-10 2177  ax-11 2193  ax-12 2206  ax-13 2411  ax-ext 2754

This theorem depends on definitions:  df-bi 198  df-an 384  df-or 864  df-tru 1637  df-ex 1856  df-nf 1861  df-sb 2053  df-clab 2761  df-cleq 2767  df-clel 2770  df-nfc 2905  df-ral 3069  df-v 3357  df-in 3736  df-ss 3743  df-uni 4586  df-tr 4900  df-ord 5880

This theorem is referenced by:  onfr  5917  onelss  5920  ordtri2or2  5977  onfununi  7612  smores3  7624  tfrlem1  7646  tfrlem9a  7656  tz7.44-2  7677  tz7.44-3  7678  oaabslem  7898  oaabs2  7900  omabslem  7901  omabs  7902  findcard3  8380  nnsdomg  8396  ordiso2  8597  ordtypelem2  8601  ordtypelem6  8605  ordtypelem7  8606  cantnf  8775  cnfcomlem  8781  cardmin2  9045  infxpenlem  9057  iunfictbso  9158  dfac12lem2  9189  dfac12lem3  9190  unctb  9250  ackbij2lem1  9264  ackbij1lem3  9267  ackbij1lem18  9282  ackbij2  9288  ttukeylem6  9559  ttukeylem7  9560  alephexp1  9624  fpwwe2lem8  9682  pwfseqlem3  9705  pwcdandom  9712  fz1isolem  13469  onsuct0  32794  finxpreclem4  33585