Theorem onelss 6366

Description: An element of an ordinal number is a subset of the number. (Contributed by NM, 5-Jun-1994.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)

Assertion

Ref	Expression
onelss	⊢ (𝐴 ∈ On → (𝐵 ∈ 𝐴 → 𝐵 ⊆ 𝐴))

Proof of Theorem onelss

Step	Hyp	Ref	Expression
1		eloni 6334	. 2 ⊢ (𝐴 ∈ On → Ord 𝐴)
2		ordelss 6340	. . 3 ⊢ ((Ord 𝐴 ∧ 𝐵 ∈ 𝐴) → 𝐵 ⊆ 𝐴)
3	2	ex 412	. 2 ⊢ (Ord 𝐴 → (𝐵 ∈ 𝐴 → 𝐵 ⊆ 𝐴))
4	1, 3	syl 17	1 ⊢ (𝐴 ∈ On → (𝐵 ∈ 𝐴 → 𝐵 ⊆ 𝐴))

Syntax hints:   → wi 4   ∈ wcel 2114   ⊆ wss 3890  Ord word 6323  Oncon0 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 3432  df-ss 3907  df-uni 4852  df-tr 5194  df-po 5539  df-so 5540  df-fr 5584  df-we 5586  df-ord 6327  df-on 6328

This theorem is referenced by:  ordunidif  6374  onelssi  6440  ssorduni  7733  tfisi  7810  poseq  8108  tfrlem9  8324  tfrlem11  8327  oaordex  8493  oaass  8496  odi  8514  omass  8515  oewordri  8528  nnaordex  8574  domtriord  9061  hartogs  9459  card2on  9469  tskwe  9874  infxpenlem  9935  cfub  10171  cfsuc  10179  coflim  10183  hsmexlem2  10349  ondomon  10485  pwcfsdom  10506  inar1  10698  tskord  10703  grudomon  10740  gruina  10741  ltsres  27626  nosupno  27667  nosupbday  27669  noinfno  27682  oldssmade  27859  madebday  27892  mulsproplem13  28120  mulsproplem14  28121  dfrdg2  35975  aomclem6  43487  nnoeomeqom  43740  naddgeoa  43822  naddwordnexlem1  43825  naddwordnexlem4  43829  iscard5  43963