Theorem 0ss 4304

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 4247	. . 3 ⊢ ¬ 𝑥 ∈ ∅
2	1	pm2.21i 119	. 2 ⊢ (𝑥 ∈ ∅ → 𝑥 ∈ 𝐴)
3	2	ssriv 3919	1 ⊢ ∅ ⊆ 𝐴

Syntax hints:   ∈ wcel 2111   ⊆ wss 3881  ∅c0 4243

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-dif 3884  df-in 3888  df-ss 3898  df-nul 4244

This theorem is referenced by:  ss0b  4305  0pss  4352  npss0  4353  ssdifeq0  4390  pwpw0  4706  sssn  4719  sspr  4726  sstp  4727  pwsnOLD  4793  uni0  4828  int0el  4869  0disj  5022  disjx0  5024  tr0  5147  al0ssb  5176  0elpw  5221  rel0  5636  0ima  5913  dmxpss  5995  dmsnopss  6038  on0eqel  6276  iotassuni  6303  fun0  6389  f0  6534  fvmptss  6757  fvmptss2  6770  funressn  6898  riotassuni  7133  frxp  7803  suppssdm  7826  suppun  7833  suppss  7843  suppssov1  7845  suppss2  7847  suppssfv  7849  oaword1  8161  oaword2  8162  omwordri  8181  oewordri  8201  oeworde  8202  nnaword1  8238  0domg  8628  fodomr  8652  pwdom  8653  php  8685  isinf  8715  finsschain  8815  fipwuni  8874  fipwss  8877  wdompwdom  9026  inf3lemd  9074  inf3lem1  9075  cantnfle  9118  tc0  9173  r1val1  9199  alephgeom  9493  infmap2  9629  cfub  9660  cf0  9662  cflecard  9664  cfle  9665  fin23lem16  9746  itunitc1  9831  ttukeylem6  9925  ttukeylem7  9926  canthwe  10062  wun0  10129  tsk0  10174  gruina  10229  grur1a  10230  uzssz  12252  xrsup0  12704  fzoss1  13059  fsuppmapnn0fiubex  13355  swrd00  13997  swrdlend  14006  repswswrd  14137  xptrrel  14331  relexpdmd  14395  relexprnd  14399  relexpfldd  14401  rtrclreclem4  14412  sum0  15070  fsumss  15074  fsumcvg3  15078  prod0  15289  0bits  15778  sadid1  15807  sadid2  15808  smu01lem  15824  smu01  15825  smu02  15826  lcmf0  15968  vdwmc2  16305  vdwlem13  16319  ramz2  16350  strfvss  16498  ressbasss  16548  ress0  16550  ismred2  16866  acsfn  16922  acsfn0  16923  0ssc  17099  fullfunc  17168  fthfunc  17169  mrelatglb0  17787  cntzssv  18450  symgsssg  18587  efgsfo  18857  dprdsn  19151  lsp0  19774  lss0v  19781  lspsnat  19910  lsppratlem3  19914  lbsexg  19929  evpmss  20275  ocv0  20366  ocvz  20367  css1  20379  resspsrbas  20653  mhp0cl  20797  psr1crng  20816  psr1assa  20817  psr1tos  20818  psr1bas2  20819  vr1cl2  20822  ply1lss  20825  ply1subrg  20826  psr1plusg  20851  psr1vsca  20852  psr1mulr  20853  psr1ring  20876  psr1lmod  20878  psr1sca  20879  0opn  21509  toponsspwpw  21527  basdif0  21558  baspartn  21559  0cld  21643  ntr0  21686  cmpfi  22013  refun0  22120  xkouni  22204  xkoccn  22224  alexsubALTlem2  22653  ptcmplem2  22658  tsmsfbas  22733  setsmstopn  23085  restmetu  23177  tngtopn  23256  iccntr  23426  xrge0gsumle  23438  xrge0tsms  23439  metdstri  23456  ovol0  24097  0mbl  24143  itg1le  24317  itgioo  24419  limcnlp  24481  dvbsss  24505  plyssc  24797  fsumharmonic  25597  egrsubgr  27067  0grsubgr  27068  0uhgrsubgr  27069  chocnul  29111  span0  29325  chsup0  29331  ssnnssfz  30536  xrge0tsmsd  30742  ddemeas  31605  dya2iocuni  31651  oms0  31665  0elcarsg  31675  eulerpartlemt  31739  bnj1143  32172  mrsubrn  32873  msubrn  32889  mthmpps  32942  dfpo2  33104  trpredlem1  33179  nulsslt  33375  nulssgt  33376  bj-nuliotaALT  34475  bj-restsn0  34500  bj-restsn10  34501  bj-imdirco  34605  pibt2  34834  mblfinlem2  35095  mblfinlem3  35096  ismblfin  35098  sstotbnd2  35212  isbnd3  35222  ssbnd  35226  heiborlem6  35254  lub0N  36485  glb0N  36489  0psubN  37045  padd01  37107  padd02  37108  pol0N  37205  pcl0N  37218  0psubclN  37239  mzpcompact2lem  39692  itgocn  40108  fvnonrel  40297  clcnvlem  40323  cnvrcl0  40325  cnvtrcl0  40326  0he  40483  ntrclskb  40772  gru0eld  40937  mnu0eld  40973  mnuprdlem4  40983  mnuprd  40984  founiiun0  41817  uzfissfz  41958  limcdm0  42260  cncfiooicc  42536  itgvol0  42610  ibliooicc  42613  ovn0  43205  sprssspr  43998  ssnn0ssfz  44751  setrec2fun  45222