Theorem 0ss 3814

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

Assertion

Ref	Expression
0ss

Proof of Theorem 0ss

Dummy variable is distinct from all other variables.

Step	Hyp	Ref	Expression
1		noel 3788	. . 3
2	1	pm2.21i 131	. 2
3	2	ssriv 3507	1

Syntax hints:  e.wcel 1818  C_wss 3475  c0 3784

This theorem is referenced by:  ss0b  3815  0pss  3864  npss0  3865  ssdifeq0  3910  pwpw0  4178  sssn  4188  sspr  4193  sstp  4194  pwsnALT  4244  uni0  4276  int0el  4318  0disj  4445  disjx0  4447  tr0  4556  0elpw  4621  on0eqel  5000  rel0  5132  0ima  5358  dmxpss  5443  dmsnopss  5485  iotassuni  5572  fun0  5650  fresaunres2  5762  f0  5771  fvmptss  5964  fvmptss2  5975  funressn  6084  riotassuniOLD  6294  frxp  6910  suppssdm  6931  suppun  6939  suppss  6949  suppssov1  6951  suppss2  6953  suppssfv  6955  oaword1  7220  oaword2  7221  omwordri  7240  oewordri  7260  oeworde  7261  nnaword1  7297  0domg  7664  fodomr  7688  pwdom  7689  php  7721  isinf  7753  finsschain  7847  fipwuni  7906  fipwss  7909  wdompwdom  8025  inf3lemd  8065  inf3lem1  8066  cantnfle  8111  cantnfleOLD  8141  tc0  8199  r1val1  8225  alephgeom  8484  infmap2  8619  cfub  8650  cf0  8652  cflecard  8654  cfle  8655  fin23lem16  8736  itunitc1  8821  ttukeylem6  8915  ttukeylem7  8916  canthwe  9050  wun0  9117  tsk0  9162  gruina  9217  grur1a  9218  uzssz  11129  xrsup0  11544  fzoss1  11852  fsuppmapnn0fiubex  12098  swrd00  12645  swrdlend  12656  swrd0  12658  repswswrd  12756  sum0  13543  fsumss  13547  fsumcvg3  13551  prod0  13750  0bits  14089  sadid1  14118  sadid2  14119  smu01lem  14135  smu01  14136  smu02  14137  vdwmc2  14497  vdwlem13  14511  ramz2  14542  strfvss  14650  ressbasss  14689  ress0  14691  strlemor0  14723  ismred2  15000  acsfn  15056  acsfn0  15057  0ssc  15206  fullfunc  15275  fthfunc  15276  mrelatglb0  15815  cntzssv  16366  symgsssg  16492  efgsfo  16757  dprdsn  17083  lsp0  17655  lss0v  17662  lspsnat  17791  lsppratlem3  17795  lbsexg  17810  resspsrbas  18070  psr1crng  18226  psr1assa  18227  psr1tos  18228  psr1bas2  18229  vr1cl2  18232  ply1lss  18235  ply1subrg  18236  psr1plusg  18263  psr1vsca  18264  psr1mulr  18265  psr1ring  18288  psr1lmod  18290  psr1sca  18291  evpmss  18622  ocv0  18708  ocvz  18709  css1  18721  0opn  19413  basdif0  19454  baspartn  19455  0cld  19539  cls0  19581  ntr0  19582  cmpfi  19908  refun0  20016  xkouni  20100  xkoccn  20120  filcon  20384  alexsubALTlem2  20548  ptcmplem2  20553  tsmsfbas  20626  setsmstopn  20981  restmetu  21090  tngtopn  21164  iccntr  21326  xrge0gsumle  21338  xrge0tsms  21339  metdstri  21355  ovol0  21904  0mbl  21950  itg1le  22120  itgioo  22222  limcnlp  22282  dvbsss  22306  plyssc  22597  fsumharmonic  23341  chocnul  26246  span0  26460  chsup0  26466  ssnnssfz  27597  xrge0tsmsd  27775  ddemeas  28208  dya2iocuni  28254  oms0  28266  eulerpartlemt  28310  mrsubrn  28873  msubrn  28889  mthmpps  28942  dfpo2  29184  trpredlem1  29310  mblfinlem2  30052  mblfinlem3  30053  ismblfin  30055  sstotbnd2  30270  isbnd3  30280  ssbnd  30284  heiborlem6  30312  mzpcompact2lem  30684  itgocn  31113  limcdm0  31624  cncfiooicc  31697  itgvol0  31767  ibliooicc  31770  ssnn0ssfz  32938  bnj1143  33849  bj-nuliotaALT  34587  lub0N  34914  glb0N  34918  0psubN  35473  padd01  35535  padd02  35536  pol0N  35633  pcl0N  35646  0psubclN  35667  xptrrel  37775  0he  37805

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-v 3111  df-dif 3478  df-in 3482  df-ss 3489  df-nul 3785