Theorem onsseleq 6356

Description: Relationship between subset and membership of an ordinal number. (Contributed by NM, 15-Sep-1995.)

Assertion

Ref	Expression
onsseleq	⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ⊆ 𝐵 ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵)))

Proof of Theorem onsseleq

Step	Hyp	Ref	Expression
1		eloni 6325	. 2 ⊢ (𝐴 ∈ On → Ord 𝐴)
2		eloni 6325	. 2 ⊢ (𝐵 ∈ On → Ord 𝐵)
3		ordsseleq 6344	. 2 ⊢ ((Ord 𝐴 ∧ Ord 𝐵) → (𝐴 ⊆ 𝐵 ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵)))
4	1, 2, 3	syl2an 596	1 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ⊆ 𝐵 ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵)))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 847   = wceq 1541   ∈ wcel 2113   ⊆ wss 3899  Ord word 6314  Oncon0 6315

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706  ax-sep 5239  ax-nul 5249  ax-pr 5375

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-ne 2931  df-ral 3050  df-rex 3059  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4284  df-if 4478  df-pw 4554  df-sn 4579  df-pr 4581  df-op 4585  df-uni 4862  df-br 5097  df-opab 5159  df-tr 5204  df-eprel 5522  df-po 5530  df-so 5531  df-fr 5575  df-we 5577  df-ord 6318  df-on 6319

This theorem is referenced by:  onsseli  6437  on0eqel  6440  onmindif2  7750  omword  8495  oeword  8516  oewordi  8517  dffi3  9332  cantnflem1d  9595  cantnflem1  9596  r1ord3g  9689  alephdom  9989  cardaleph  9997  cfsmolem  10178  ttukeylem5  10421  alephreg  10491  inar1  10684  gruina  10727  om2uzlt2i  13872  nolt02o  27661  nogt01o  27662  nosupbnd2lem1  27681  noinfbnd2lem1  27696  madebday  27872  om2noseqlt2  28261  oege2  43491  ontric3g  43705