Theorem 0ss 3452

Description: The null set is a subset of any class. Part of Exercise 1 of [TakeutiZaring] p. 22. (Contributed by NM, 5-Aug-1993.)

Assertion

Ref	Expression
0ss	|- (/) C_ A

Proof of Theorem 0ss

Dummy variable x is distinct from all other variables.

Step	Hyp	Ref	Expression
1		noel 3418	. . 3 |- -. x e. (/)
2	1	pm2.21i 641	. 2 |- ( x e. (/) -> x e. A )
3	2	ssriv 3151	1 |- (/) C_ A

Syntax hints:   e. wcel 2141   C_ wss 3121   (/)c0 3414

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 609  ax-in2 610  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-tru 1351  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-v 2732  df-dif 3123  df-in 3127  df-ss 3134  df-nul 3415

This theorem is referenced by:  ss0b  3453  ssdifeq0  3496  sssnr  3738  ssprr  3741  uni0  3821  int0el  3859  0disj  3984  disjx0  3986  tr0  4096  0elpw  4148  exmidsssn  4186  fr0  4334  elomssom  4587  rel0  4734  0ima  4969  fun0  5254  f0  5386  el2oss1o  6419  oaword1  6447  0domg  6811  nnnninf  7098  exmidfodomrlemim  7165  pw1on  7190  sum0  11338  prod0  11535  ennnfonelemj0  12343  ennnfonelemkh  12354  0opn  12757  baspartn  12801  0cld  12865  ntr0  12887  bdeq0  13862  bj-omtrans  13951  nninfsellemsuc  14005