Theorem ordelss 6404

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 6402	. 2 ⊢ (Ord 𝐴 → Tr 𝐴)
2		trss 5228	. . 3 ⊢ (Tr 𝐴 → (𝐵 ∈ 𝐴 → 𝐵 ⊆ 𝐴))
3	2	imp 412	. 2 ⊢ ((Tr 𝐴 ∧ 𝐵 ∈ 𝐴) → 𝐵 ⊆ 𝐴)
4	1, 3	sylan 592	1 ⊢ ((Ord 𝐴 ∧ 𝐵 ∈ 𝐴) → 𝐵 ⊆ 𝐴)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2147   ⊆ wss 3900  Tr wtr 5218  Ord word 6387

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ral 3081  df-v 3456  df-ss 3901  df-uni 4873  df-tr 5219  df-ord 6391

This theorem is used by:  onfr  6428  onelss  6431  ordtri2or2  6490  onfununi  8387  smores3  8399  tfrlem1  8421  tfrlem9a  8432  tz7.44-2  8453  tz7.44-3  8454  oaabslem  8694  oaabs2  8696  omabslem  8697  omabs  8698  findcard3  9312  nnsdomg  9329  ordiso2  9546  ordtypelem2  9550  ordtypelem6  9554  ordtypelem7  9555  cantnf  9731  cnfcomlem  9737  ttrcltr  9754  cardmin2  10119  infxpenlem  10131  iunfictbso  10232  dfac12lem2  10262  dfac12lem3  10263  unctb  10321  ackbij2lem1  10335  ackbij1lem3  10338  ackbij1lem18  10353  ackbij2  10359  ttukeylem6  10631  ttukeylem7  10632  alephexp1  10703  fpwwe2lem7  10761  pwfseqlem3  10784  pwdjundom  10791  fz1isolem  14647  noinfbday  28134  onsuct0  37444  finxpreclem4  38585  nadd2rabtr  44647  grur1cld  45491