Theorem omsson 7849

Description: Omega is a subset of On. (Contributed by NM, 13-Jun-1994.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)

Assertion

Ref	Expression
omsson	⊢ ω ⊆ On

Proof of Theorem omsson

Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-om 7846	. 2 ⊢ ω = {𝑥 ∈ On ∣ ∀𝑦(Lim 𝑦 → 𝑥 ∈ 𝑦)}
2	1	ssrab3 4048	1 ⊢ ω ⊆ On

Syntax hints:   → wi 4  ∀wal 1538   ⊆ wss 3917  Oncon0 6335  Lim wlim 6336  ωcom 7845

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-rab 3409  df-ss 3934  df-om 7846

This theorem is referenced by:  limomss  7850  nnon  7851  ordom  7855  omssnlim  7860  omsinds  7866  nnunifi  9245  unblem1  9246  unblem2  9247  unblem3  9248  unblem4  9249  isfinite2  9252  card2inf  9515  ackbij1lem16  10194  ackbij1lem18  10196  fin23lem26  10285  fin23lem27  10288  isf32lem5  10317  fin1a2lem6  10365  pwfseqlem3  10620  tskinf  10729  grothomex  10789  ltsopi  10848  dmaddpi  10850  dmmulpi  10851  2ndcdisj  23350  finminlem  36313  cantnftermord  43316  omabs2  43328