Theorem 0ss 4336

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

Syntax hints:   ∈ wcel 2110   ⊆ wss 3892  ∅c0 4262

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-8 2112  ax-9 2120  ax-ext 2711

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1545  df-fal 1555  df-ex 1787  df-sb 2072  df-clab 2718  df-cleq 2732  df-clel 2818  df-v 3433  df-dif 3895  df-in 3899  df-ss 3909  df-nul 4263

This theorem is referenced by:  ss0b  4337  0pss  4384  npss0  4385  ssdifeq0  4423  pwpw0  4752  sssn  4765  sspr  4772  sstp  4773  pwsnOLD  4838  uni0  4875  int0el  4916  0disj  5071  disjx0  5073  tr0  5207  al0ssb  5236  0elpw  5282  rel0  5708  0ima  5985  dmxpss  6073  dmsnopss  6116  dfpo2  6198  on0eqel  6383  iotassuni  6411  fun0  6497  f0  6653  fvmptss  6884  fvmptss2  6897  funressn  7028  riotassuni  7270  frxp  7959  suppssdm  7985  suppun  7992  suppss  8002  suppssOLD  8003  suppssov1  8006  suppss2  8008  suppssfv  8010  oaword1  8375  oaword2  8376  omwordri  8395  oewordri  8415  oeworde  8416  nnaword1  8452  mapssfset  8631  0domgOLD  8879  fodomr  8906  pwdom  8907  php  8983  phpOLD  8995  isinf  9024  finsschain  9114  fipwuni  9173  fipwss  9176  wdompwdom  9325  inf3lemd  9373  inf3lem1  9374  cantnfle  9417  ttrclselem1  9471  trpredlem1  9484  tc0  9515  r1val1  9555  alephgeom  9849  infmap2  9985  cfub  10016  cf0  10018  cflecard  10020  cfle  10021  fin23lem16  10102  itunitc1  10187  ttukeylem6  10281  ttukeylem7  10282  canthwe  10418  wun0  10485  tsk0  10530  gruina  10585  grur1a  10586  uzssz  12614  xrsup0  13068  fzoss1  13425  fsuppmapnn0fiubex  13723  swrd00  14368  swrdlend  14377  repswswrd  14508  xptrrel  14702  relexpdmd  14766  relexprnd  14770  relexpfldd  14772  rtrclreclem4  14783  sum0  15444  fsumss  15448  fsumcvg3  15452  prod0  15664  0bits  16157  sadid1  16186  sadid2  16187  smu01lem  16203  smu01  16204  smu02  16205  lcmf0  16350  vdwmc2  16691  vdwlem13  16705  ramz2  16736  strfvss  16899  ressbasss  16961  ress0  16964  ismred2  17323  acsfn  17379  acsfn0  17380  0ssc  17563  fullfunc  17633  fthfunc  17634  mrelatglb0  18290  cntzssv  18945  symgsssg  19086  efgsfo  19356  dprdsn  19650  lsp0  20282  lss0v  20289  lspsnat  20418  lsppratlem3  20422  lbsexg  20437  evpmss  20802  ocv0  20893  ocvz  20894  css1  20906  resspsrbas  21195  mhp0cl  21347  psr1crng  21369  psr1assa  21370  psr1tos  21371  psr1bas2  21372  vr1cl2  21375  ply1lss  21378  ply1subrg  21379  psr1plusg  21404  psr1vsca  21405  psr1mulr  21406  psr1ring  21429  psr1lmod  21431  psr1sca  21432  0opn  22064  toponsspwpw  22082  basdif0  22114  baspartn  22115  0cld  22200  ntr0  22243  cmpfi  22570  refun0  22677  xkouni  22761  xkoccn  22781  alexsubALTlem2  23210  ptcmplem2  23215  tsmsfbas  23290  setsmstopn  23644  restmetu  23737  tngtopn  23825  iccntr  23995  xrge0gsumle  24007  xrge0tsms  24008  metdstri  24025  ovol0  24668  0mbl  24714  itg1le  24889  itgioo  24991  limcnlp  25053  dvbsss  25077  plyssc  25372  fsumharmonic  26172  egrsubgr  27655  0grsubgr  27656  0uhgrsubgr  27657  chocnul  29699  span0  29913  chsup0  29919  ssnnssfz  31117  xrge0tsmsd  31326  ddemeas  32213  dya2iocuni  32259  oms0  32273  0elcarsg  32283  eulerpartlemt  32347  bnj1143  32779  mrsubrn  33484  msubrn  33500  mthmpps  33553  nulsslt  34000  nulssgt  34001  bday0b  34033  madess  34068  oldssmade  34069  bj-nuliotaALT  35238  bj-restsn0  35265  bj-restsn10  35266  bj-imdirco  35370  pibt2  35597  mblfinlem2  35824  mblfinlem3  35825  ismblfin  35827  sstotbnd2  35941  isbnd3  35951  ssbnd  35955  heiborlem6  35983  lub0N  37212  glb0N  37216  0psubN  37772  padd01  37834  padd02  37835  pol0N  37932  pcl0N  37945  0psubclN  37966  sn-iotassuni  40205  mzpcompact2lem  40582  itgocn  40998  fvnonrel  41187  clcnvlem  41213  cnvrcl0  41215  cnvtrcl0  41216  0he  41372  ntrclskb  41661  gru0eld  41829  mnu0eld  41865  mnuprdlem4  41875  mnuprd  41876  founiiun0  42710  uzfissfz  42847  limcdm0  43141  cncfiooicc  43417  itgvol0  43491  ibliooicc  43494  ovn0  44086  sprssspr  44912  ssnn0ssfz  45664  ipolub0  46257  ipoglb0  46259  setrec2fun  46377