Theorem 0ss 1725

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 1711	. . 3 |- -. x e. (/)
2	1	pm2.21i 73	. 2 |- (x e. (/) -> x e. A)
3	2	ssriv 1508	1 |- (/) (_ A

Syntax hints:   e. wcel 1092   (_ wss 1487  (/)c0 1707

This theorem is referenced by:  ss0b 1726  0pss 1730  sssn 1852  snsspr 1853  pw0 1882  pwpw0 1883  uni0 1938  int0el 1985  tr0 2052  on0eqelt 2370  rel0 2499  fun0 2691  f0 2772  oaword1 3154  oaword2 3155  nnmordi 3188  map0e 3266  0dom 3366  php 3409  inf3lemd 3463  inf3lem1 3464  r1val1 3502  fodomb 3615  alephgeom 3687  cfub 3703  cf0 3705  cflecard 3707  cfle 3708  infxpidmlem8 4940  infmap2 4953  chocnul 5293  span0 5448  chsup0 5453

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-16 922  ax-17 925  ax-ext 1074

This theorem depends on definitions:  df-bi 128  df-or 197  df-an 198  df-ex 679  df-sb 853  df-clab 1093  df-cleq 1097  df-clel 1099  df-v 1349  df-dif 1489  df-in 1491  df-ss 1492  df-nul 1708

metamath.org