Theorem 0ss 2297

Description: The null set is a subset of any class. Part of Exercise 1 of [TakeutiZaring] p. 22.

Assertion

Ref	Expression
0ss	|- (/) (_ A

Proof of Theorem 0ss

Step	Hyp	Ref	Expression
1		noel 2280	. . 3 |- -. x e. (/)
2	1	pm2.21i 77	. 2 |- (x e. (/) -> x e. A)
3	2	ssriv 2065	1 |- (/) (_ A

Syntax hints:   e. wcel 956   (_ wss 2043  (/)c0 2276

This theorem is referenced by:  ss0b 2298  0pss 2304  pwpw0 2465  snsspr 2466  sssn 2469  sspr 2471  uni0 2520  int0el 2556  tr0 2686  0elpw 2731  on0eqelt 3119  rel0 3267  0ima 3413  dmxpss 3465  rnxpss 3466  fun0 3536  f0 3647  oaword1 4176  oaword2 4177  omwordri 4193  oewordri 4209  oeworde 4210  mapsspw 4331  map0e 4332  0dom 4450  fodomr 4469  php 4499  inf3lemd 4592  inf3lem1 4593  r1val1 4638  alephgeom 4862  cfub 4888  cf0 4890  cflecard 4892  cfle 4893  xrsup0 6052  ioossre 6336  uzssz 6370  infxpidmlem8 7510  infmap2 7531  0opnt 7551  0cld 7628  cls0 7659  ntr0 7660  chocnul 9230  span0 9403  chsup0 9409  clsrebb 10416

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-8 962  ax-10 964  ax-12 966  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-10o 1138  ax-16 1208  ax-11o 1216  ax-ext 1457

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 979  df-sb 1170  df-clab 1462  df-cleq 1467  df-clel 1470  df-v 1808  df-dif 2045  df-in 2047  df-ss 2049  df-nul 2277

Copyright terms: Public domain