Theorem omsson 7905

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 7902	. 2 ⊢ ω = {𝑥 ∈ On ∣ ∀𝑦(Lim 𝑦 → 𝑥 ∈ 𝑦)}
2	1	ssrab3 4010	1 ⊢ ω ⊆ On

This proof depends on syntax axioms:   → wi 4  ∀wal 1568   ⊆ wss 3900  Oncon0 6380  Lim wlim 6381  ωcom 7901

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-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-ss 3901  df-om 7902

This theorem is used by:  limomss  7906  nnon  7907  ordom  7911  omssnlim  7916  omsinds  7922  nnunifi  9311  unblem1  9312  unblem2  9313  unblem3  9314  unblem4  9315  isfinite2  9318  card2inf  9576  ackbij1lem16  10339  ackbij1lem18  10341  fin23lem26  10430  fin23lem27  10433  isf32lem5  10462  fin1a2lem6  10510  pwfseqlem3  10772  tskinf  10881  grothomex  10941  ltsopi  11000  dmaddpi  11002  dmmulpi  11003  2ndcdisj  23805  finminlem  37284  ttcid  37458  dfttc2g  37472  mh-inf3f1  37507  cantnftermord  44514  omabs2  44526