Home

Metamath Proof Explorer

< Previous   Next > Related theorems Unicode version

---

Theorem 0ss 2291

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

Assertion

Ref	Expression
0ss

---

Proof of Theorem 0ss

Step	Hyp	Ref	Expression
1		noel 2274	. . 3
2	1	pm2.21i 77	. 2
3	2	ssriv 2059	1

Colors of variables: wff set class

Syntax hints:   wcel 955   wss 2037  c0 2270

This theorem is referenced by:  ss0b 2292  0pss 2298  pwpw0 2460  snsspr 2461  sssn 2464  sspr 2466  uni0 2515  int0el 2551  tr0 2681  0elpw 2726  on0eqelt 3114  rel0 3262  0ima 3405  dmxpss 3459  rnxpss 3460  fun0 3530  f0 3641  oaword1 4170  oaword2 4171  omwordri 4187  oewordri 4203  oeworde 4204  mapsspw 4325  map0e 4326  0dom 4444  fodomr 4463  php 4493  inf3lemd 4584  inf3lem1 4585  r1val1 4630  alephgeom 4854  cfub 4880  cf0 4882  cflecard 4884  cfle 4885  xrsup0 6044  ioossre 6328  uzssz 6362  infxpidmlem8 7502  infmap2 7523  0opnt 7543  0cld 7620  cls0 7651  chocnul 9207  span0 9380  chsup0 9386  clsrebb 10380

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 959  ax-gen 960  ax-8 961  ax-10 963  ax-12 965  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975  ax-9o 1119  ax-10o 1136  ax-16 1206  ax-11o 1213  ax-ext 1452

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 978  df-sb 1168  df-clab 1457  df-cleq 1462  df-clel 1465  df-v 1803  df-dif 2039  df-in 2041  df-ss 2043  df-nul 2271

Copyright terms: Public domain