Theorem 0ss 2900

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

Assertion

Ref	Expression
0ss	|- (/) C_ A

Proof of Theorem 0ss

Step	Hyp	Ref	Expression
1		noel 2879	. . 3 |- -. x e. (/)
2	1	pm2.21i 93	. 2 |- (x e. (/) -> x e. A)
3	2	ssriv 2621	1 |- (/) C_ A

Syntax hints:   e. wcel 1300   C_ wss 2593  (/)c0 2875

This theorem is referenced by:  ss0b 2901  0pss 2910  npss0 2911  pwpw0 3134  snsspr1OLD 3136  sssn 3142  sspr 3144  pwsnALT 3173  uni0 3205  int0el 3248  tr0 3423  0elpw 3473  on0eqel 3787  rel0 4102  0ima 4284  dmxpss 4343  rnxpssOLD 4345  fun0 4472  f0 4600  oaword1 5234  oaword2 5235  omwordri 5251  oewordri 5267  oeworde 5268  mapsspw 5400  map0e 5401  0dom 5527  fodomr 5547  php 5607  inf3lemd 5718  inf3lem1 5719  r1val1 5769  omsublim 5887  alephgeom 6030  cfub 6056  cf0 6058  cflecard 6060  cfle 6061  xrsup0 7306  uzssz 7599  infxpidmlem8 8828  infmap2 8850  0opn 8870  0cld 8954  cls0 8985  ntr0 8986  vacnlem4 9670  indexfi 10174  stoig 10251  chocnul 10925  span0 11098  chsup0 11104  bnj1143 12942  trcllem1 13933  frxp 13951  imfstnrelc 14396  clsrebb 14844  oibbi1 14853  oibbi2 14854  sallnei 14873  rcfpfillem3 14930  rcfpfillem5 14932  clindistop 14962  finsschain 15373  omsublimOLD 15396  alexsublem2 15438  reconnlem1 15446  indexfiOLD 15755  heiborlem21 15975  rrntotbnd 16022  smoge 16454  glb0 16920  0psub 17230  padd01 17272  padd02 17273  pol0 17322  0psubcl 17352

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-ex 1327  df-sb 1536  df-clab 1872  df-cleq 1877  df-clel 1880  df-v 2294  df-dif 2597  df-in 2603  df-ss 2605  df-nul 2876

Copyright terms: Public domain