Theorem 0ss 3249

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 3222	. . 3 |- -. x e. (/)
2	1	pm2.21i 574	. 2 |- (x e. (/) -> x e. A)
3	2	ssriv 2943	1 |- (/) C_ A

Syntax hints:   e. wcel 1390   C_ wss 2911   (/)c0 3218

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-in1 544  ax-in2 545  ax-io 629  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-10 1393  ax-11 1394  ax-i12 1395  ax-bndl 1396  ax-4 1397  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019

This theorem depends on definitions:  df-bi 110  df-tru 1245  df-nf 1347  df-sb 1643  df-clab 2024  df-cleq 2030  df-clel 2033  df-nfc 2164  df-v 2553  df-dif 2914  df-in 2918  df-ss 2925  df-nul 3219

This theorem is referenced by:  ss0b  3250  0pss  3259  npss0  3260  ssdifeq0  3299  sssnr  3515  ssprr  3518  uni0  3598  int0el  3636  0disj  3752  disjx0  3754  tr0  3856  0elpw  3908  elnn  4271  rel0  4405  0ima  4628  fun0  4900  f0  5023  oaword1  5989  bdeq0  9322  bj-omtrans  9416