Theorem ordelss 6339

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 6337	. 2 ⊢ (Ord 𝐴 → Tr 𝐴)
2		trss 5202	. . 3 ⊢ (Tr 𝐴 → (𝐵 ∈ 𝐴 → 𝐵 ⊆ 𝐴))
3	2	imp 406	. 2 ⊢ ((Tr 𝐴 ∧ 𝐵 ∈ 𝐴) → 𝐵 ⊆ 𝐴)
4	1, 3	sylan 581	1 ⊢ ((Ord 𝐴 ∧ 𝐵 ∈ 𝐴) → 𝐵 ⊆ 𝐴)

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2114   ⊆ wss 3889  Tr wtr 5192  Ord word 6322

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-ral 3052  df-v 3431  df-ss 3906  df-uni 4851  df-tr 5193  df-ord 6326

This theorem is referenced by:  onfr  6362  onelss  6365  ordtri2or2  6424  onfununi  8281  smores3  8293  tfrlem1  8315  tfrlem9a  8325  tz7.44-2  8346  tz7.44-3  8347  oaabslem  8583  oaabs2  8585  omabslem  8586  omabs  8587  findcard3  9193  nnsdomg  9209  ordiso2  9430  ordtypelem2  9434  ordtypelem6  9438  ordtypelem7  9439  cantnf  9614  cnfcomlem  9620  ttrcltr  9637  cardmin2  9923  infxpenlem  9935  iunfictbso  10036  dfac12lem2  10067  dfac12lem3  10068  unctb  10126  ackbij2lem1  10140  ackbij1lem3  10143  ackbij1lem18  10158  ackbij2  10164  ttukeylem6  10436  ttukeylem7  10437  alephexp1  10502  fpwwe2lem7  10560  pwfseqlem3  10583  pwdjundom  10590  fz1isolem  14423  noinfbday  27684  onsuct0  36623  finxpreclem4  37710  nadd2rabtr  43812  grur1cld  44659