Theorem ordelss 6341

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2114   ⊆ wss 3903  Tr wtr 5207  Ord word 6324

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 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-v 3444  df-ss 3920  df-uni 4866  df-tr 5208  df-ord 6328

This theorem is referenced by:  onfr  6364  onelss  6367  ordtri2or2  6426  onfununi  8283  smores3  8295  tfrlem1  8317  tfrlem9a  8327  tz7.44-2  8348  tz7.44-3  8349  oaabslem  8585  oaabs2  8587  omabslem  8588  omabs  8589  findcard3  9195  nnsdomg  9211  ordiso2  9432  ordtypelem2  9436  ordtypelem6  9440  ordtypelem7  9441  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  14396  noinfbday  27700  onsuct0  36657  finxpreclem4  37649  nadd2rabtr  43741  grur1cld  44588