Theorem 0ss 3499

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 3464	. . 3 |- -. x e. (/)
2	1	pm2.21i 647	. 2 |- ( x e. (/) -> x e. A )
3	2	ssriv 3197	1 |- (/) C_ A

Syntax hints:   e. wcel 2176   C_ wss 3166   (/)c0 3460

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 615  ax-in2 616  ax-io 711  ax-5 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-nfc 2337  df-v 2774  df-dif 3168  df-in 3172  df-ss 3179  df-nul 3461

This theorem is referenced by:  ss0b  3500  ssdifeq0  3543  sssnr  3794  ssprr  3797  uni0  3877  int0el  3915  0disj  4041  disjx0  4043  tr0  4153  0elpw  4208  exmidsssn  4246  fr0  4398  elomssom  4653  rel0  4800  0ima  5042  fun0  5332  f0  5466  el2oss1o  6529  oaword1  6557  0domg  6934  nnnninf  7228  exmidfodomrlemim  7309  pw1on  7338  fzowrddc  11100  swrd00g  11102  swrdlend  11111  sum0  11699  prod0  11896  0bits  12270  ennnfonelemj0  12772  ennnfonelemkh  12783  lsp0  14185  lss0v  14192  0opn  14478  baspartn  14522  0cld  14584  ntr0  14606  bdeq0  15803  bj-omtrans  15892  nninfsellemsuc  15949  nnnninfex  15959