Theorem 0ss 4353

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

Syntax hints:   ∈ wcel 2109   ⊆ wss 3905  ∅c0 4286

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-dif 3908  df-ss 3922  df-nul 4287

This theorem is referenced by:  ss0b  4354  0pss  4400  npss0  4401  ssdifeq0  4440  pwpw0  4767  sssn  4780  sspr  4789  sstp  4790  uni0  4889  int0el  4932  0disj  5088  disjx0  5090  tr0  5214  al0ssb  5250  0elpw  5298  rel0  5746  0ima  6033  dmxpss  6124  dmsnopss  6167  dfpo2  6248  on0eqel  6436  iotassuni  6461  fun0  6551  f0  6709  fvmptss  6946  fvmptss2  6960  funressn  7097  riotassuni  7350  ordsuci  7748  frxp  8066  suppssdm  8117  suppun  8124  suppss  8134  suppssov1  8137  suppssov2  8138  suppss2  8140  suppssfv  8142  oaword1  8477  oaword2  8478  omwordri  8497  oewordri  8517  oeworde  8518  nnaword1  8554  naddword1  8616  mapssfset  8785  fodomr  9052  pwdom  9053  php  9131  isinf  9165  isinfOLD  9166  fodomfir  9237  finsschain  9268  fipwuni  9335  fipwss  9338  wdompwdom  9489  inf3lemd  9542  inf3lem1  9543  cantnfle  9586  ttrclselem1  9640  tc0  9662  r1val1  9701  alephgeom  9995  infmap2  10130  cfub  10162  cf0  10164  cflecard  10166  cfle  10167  fin23lem16  10248  itunitc1  10333  ttukeylem6  10427  ttukeylem7  10428  canthwe  10564  wun0  10631  tsk0  10676  gruina  10731  grur1a  10732  uzssz  12774  xrsup0  13243  fzoss1  13607  fsuppmapnn0fiubex  13917  swrd00  14569  swrdlend  14578  repswswrd  14708  xptrrel  14905  relexpdmd  14969  relexprnd  14973  relexpfldd  14975  rtrclreclem4  14986  sum0  15646  fsumss  15650  fsumcvg3  15654  prod0  15868  0bits  16368  sadid1  16397  sadid2  16398  smu01lem  16414  smu01  16415  smu02  16416  lcmf0  16563  vdwmc2  16909  vdwlem13  16923  ramz2  16954  strfvss  17116  ressbasssg  17166  ressbasssOLD  17169  ress0  17172  ismred2  17523  acsfn  17583  acsfn0  17584  0ssc  17762  fullfunc  17833  fthfunc  17834  mrelatglb0  18485  cntzssv  19225  symgsssg  19364  efgsfo  19636  dprdsn  19935  lsp0  20930  lss0v  20938  lspsnat  21070  lsppratlem3  21074  lbsexg  21089  evpmss  21511  ocv0  21602  ocvz  21603  css1  21615  resspsrbas  21899  mhp0cl  22049  psr1crng  22087  psr1assa  22088  psr1tos  22089  psr1bas2  22090  vr1cl2  22093  ply1lss  22097  ply1subrg  22098  psr1plusg  22121  psr1vsca  22122  psr1mulr  22123  psr1ring  22147  psr1lmod  22149  psr1sca  22150  0opn  22807  toponsspwpw  22825  basdif0  22856  baspartn  22857  0cld  22941  ntr0  22984  cmpfi  23311  refun0  23418  xkouni  23502  xkoccn  23522  alexsubALTlem2  23951  ptcmplem2  23956  tsmsfbas  24031  setsmstopn  24382  restmetu  24474  tngtopn  24554  iccntr  24726  xrge0gsumle  24738  xrge0tsms  24739  metdstri  24756  ovol0  25410  0mbl  25456  itg1le  25630  itgioo  25733  limcnlp  25795  dvbsss  25819  plyssc  26121  fsumharmonic  26938  nulsslt  27726  nulssgt  27727  bday0b  27762  madess  27808  oldssmade  27809  oldss  27810  precsexlem8  28139  egrsubgr  29240  0grsubgr  29241  0uhgrsubgr  29242  chocnul  31290  span0  31504  chsup0  31510  ssnnssfz  32743  xrge0tsmsd  33028  elrgspnlem4  33198  unitprodclb  33339  constrfiss  33720  ddemeas  34205  dya2iocuni  34253  oms0  34267  0elcarsg  34277  eulerpartlemt  34341  bnj1143  34759  mrsubrn  35488  msubrn  35504  mthmpps  35557  bj-nuliotaALT  37034  bj-restsn0  37061  bj-restsn10  37062  bj-imdirco  37166  pibt2  37393  mblfinlem2  37640  mblfinlem3  37641  ismblfin  37643  sstotbnd2  37756  isbnd3  37766  ssbnd  37770  heiborlem6  37798  lub0N  39170  glb0N  39174  0psubN  39731  padd01  39793  padd02  39794  pol0N  39891  pcl0N  39904  0psubclN  39925  mzpcompact2lem  42727  itgocn  43140  oaabsb  43270  oege1  43282  nnoeomeqom  43288  cantnfresb  43300  omabs2  43308  omcl2  43309  tfsconcatb0  43320  nadd2rabex  43362  fpwfvss  43388  nla0002  43400  nla0003  43401  nla0001  43402  fvnonrel  43573  clcnvlem  43599  cnvrcl0  43601  cnvtrcl0  43602  0he  43758  ntrclskb  44045  gru0eld  44205  mnu0eld  44241  mnuprdlem4  44251  mnuprd  44252  founiiun0  45171  uzfissfz  45309  limcdm0  45603  cncfiooicc  45879  itgvol0  45953  ibliooicc  45956  ovn0  46551  sprssspr  47469  isubgr0uhgr  47861  ssnn0ssfz  48337  ipolub0  48980  ipoglb0  48982  discsubc  49053  iinfconstbas  49055  nelsubclem  49056  setc1onsubc  49591  setrec2fun  49681  setrec2mpt  49686