Theorem 0ss 3924

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

Syntax hints:   ∈ wcel 1977   ⊆ wss 3540  ∅c0 3874

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-dif 3543  df-in 3547  df-ss 3554  df-nul 3875

This theorem is referenced by:  ss0b  3925  0pss  3965  npss0  3966  npss0OLD  3967  ssdifeq0  4003  pwpw0  4284  sssn  4298  sspr  4306  sstp  4307  pwsnALT  4367  uni0  4401  int0el  4443  0disj  4575  disjx0  4577  tr0  4692  0elpw  4760  rel0  5166  0ima  5401  dmxpss  5484  dmsnopss  5525  on0eqel  5762  iotassuni  5784  fun0  5868  fresaunres2  5989  f0  5999  fvmptss  6201  fvmptss2  6212  funressn  6331  riotassuni  6547  frxp  7174  suppssdm  7195  suppun  7202  suppss  7212  suppssov1  7214  suppss2  7216  suppssfv  7218  oaword1  7519  oaword2  7520  omwordri  7539  oewordri  7559  oeworde  7560  nnaword1  7596  0domg  7972  fodomr  7996  pwdom  7997  php  8029  isinf  8058  finsschain  8156  fipwuni  8215  fipwss  8218  wdompwdom  8366  inf3lemd  8407  inf3lem1  8408  cantnfle  8451  tc0  8506  r1val1  8532  alephgeom  8788  infmap2  8923  cfub  8954  cf0  8956  cflecard  8958  cfle  8959  fin23lem16  9040  itunitc1  9125  ttukeylem6  9219  ttukeylem7  9220  canthwe  9352  wun0  9419  tsk0  9464  gruina  9519  grur1a  9520  uzssz  11583  xrsup0  12025  fzoss1  12364  fsuppmapnn0fiubex  12654  swrd00  13270  swrdlend  13283  swrd0  13286  repswswrd  13382  xptrrel  13567  sum0  14299  fsumss  14303  fsumcvg3  14307  prod0  14512  0bits  14999  sadid1  15028  sadid2  15029  smu01lem  15045  smu01  15046  smu02  15047  lcmf0  15185  vdwmc2  15521  vdwlem13  15535  ramz2  15566  strfvss  15713  ressbasss  15759  ress0  15761  strlemor0  15795  ismred2  16086  acsfn  16143  acsfn0  16144  0ssc  16320  fullfunc  16389  fthfunc  16390  mrelatglb0  17008  cntzssv  17584  symgsssg  17710  efgsfo  17975  dprdsn  18258  lsp0  18830  lss0v  18837  lspsnat  18966  lsppratlem3  18970  lbsexg  18985  resspsrbas  19236  psr1crng  19378  psr1assa  19379  psr1tos  19380  psr1bas2  19381  vr1cl2  19384  ply1lss  19387  ply1subrg  19388  psr1plusg  19413  psr1vsca  19414  psr1mulr  19415  psr1ring  19438  psr1lmod  19440  psr1sca  19441  evpmss  19751  ocv0  19840  ocvz  19841  css1  19853  0opn  20534  basdif0  20568  baspartn  20569  0cld  20652  cls0  20694  ntr0  20695  cmpfi  21021  refun0  21128  xkouni  21212  xkoccn  21232  alexsubALTlem2  21662  ptcmplem2  21667  tsmsfbas  21741  setsmstopn  22093  restmetu  22185  tngtopn  22264  iccntr  22432  xrge0gsumle  22444  xrge0tsms  22445  metdstri  22462  ovol0  23068  0mbl  23114  itg1le  23286  itgioo  23388  limcnlp  23448  dvbsss  23472  plyssc  23760  fsumharmonic  24538  chocnul  27571  span0  27785  chsup0  27791  ssnnssfz  28937  xrge0tsmsd  29116  ddemeas  29626  dya2iocuni  29672  oms0  29686  0elcarsg  29696  eulerpartlemt  29760  bnj1143  30115  mrsubrn  30664  msubrn  30680  mthmpps  30733  dfpo2  30898  trpredlem1  30971  bj-nuliotaALT  32211  bj-restsn0  32219  bj-restsn10  32220  bj-toponss  32241  mblfinlem2  32617  mblfinlem3  32618  ismblfin  32620  sstotbnd2  32743  isbnd3  32753  ssbnd  32757  heiborlem6  32785  lub0N  33494  glb0N  33498  0psubN  34053  padd01  34115  padd02  34116  pol0N  34213  pcl0N  34226  0psubclN  34247  mzpcompact2lem  36332  itgocn  36753  fvnonrel  36922  clcnvlem  36949  cnvrcl0  36951  cnvtrcl0  36952  0he  37096  ntrclskb  37387  founiiun0  38372  uzfissfz  38483  limcdm0  38685  cncfiooicc  38780  itgvol0  38860  ibliooicc  38863  ovn0  39456  egrsubgr  40501  0grsubgr  40502  0uhgrsubgr  40503  ssnn0ssfz  41920  setrec2fun  42238