Theorem 0ss 4352

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

Syntax hints:   ∈ wcel 2114   ⊆ wss 3938  ∅c0 4293

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-dif 3941  df-in 3945  df-ss 3954  df-nul 4294

This theorem is referenced by:  ss0b  4353  0pss  4398  npss0  4399  ssdifeq0  4434  pwpw0  4748  sssn  4761  sspr  4768  sstp  4769  pwsnOLD  4833  uni0  4868  int0el  4909  0disj  5060  disjx0  5062  tr0  5185  al0ssb  5214  0elpw  5258  rel0  5674  0ima  5948  dmxpss  6030  dmsnopss  6073  on0eqel  6310  iotassuni  6336  fun0  6421  f0  6562  fvmptss  6782  fvmptss2  6795  funressn  6923  riotassuni  7156  frxp  7822  suppssdm  7845  suppun  7852  suppss  7862  suppssov1  7864  suppss2  7866  suppssfv  7868  oaword1  8180  oaword2  8181  omwordri  8200  oewordri  8220  oeworde  8221  nnaword1  8257  0domg  8646  fodomr  8670  pwdom  8671  php  8703  isinf  8733  finsschain  8833  fipwuni  8892  fipwss  8895  wdompwdom  9044  inf3lemd  9092  inf3lem1  9093  cantnfle  9136  tc0  9191  r1val1  9217  alephgeom  9510  infmap2  9642  cfub  9673  cf0  9675  cflecard  9677  cfle  9678  fin23lem16  9759  itunitc1  9844  ttukeylem6  9938  ttukeylem7  9939  canthwe  10075  wun0  10142  tsk0  10187  gruina  10242  grur1a  10243  uzssz  12267  xrsup0  12719  fzoss1  13067  fsuppmapnn0fiubex  13363  swrd00  14008  swrdlend  14017  repswswrd  14148  xptrrel  14342  sum0  15080  fsumss  15084  fsumcvg3  15088  prod0  15299  0bits  15790  sadid1  15819  sadid2  15820  smu01lem  15836  smu01  15837  smu02  15838  lcmf0  15980  vdwmc2  16317  vdwlem13  16331  ramz2  16362  strfvss  16508  ressbasss  16558  ress0  16560  ismred2  16876  acsfn  16932  acsfn0  16933  0ssc  17109  fullfunc  17178  fthfunc  17179  mrelatglb0  17797  cntzssv  18460  symgsssg  18597  efgsfo  18867  dprdsn  19160  lsp0  19783  lss0v  19790  lspsnat  19919  lsppratlem3  19923  lbsexg  19938  resspsrbas  20197  mhp0cl  20339  psr1crng  20357  psr1assa  20358  psr1tos  20359  psr1bas2  20360  vr1cl2  20363  ply1lss  20366  ply1subrg  20367  psr1plusg  20392  psr1vsca  20393  psr1mulr  20394  psr1ring  20417  psr1lmod  20419  psr1sca  20420  evpmss  20732  ocv0  20823  ocvz  20824  css1  20836  0opn  21514  toponsspwpw  21532  basdif0  21563  baspartn  21564  0cld  21648  ntr0  21691  cmpfi  22018  refun0  22125  xkouni  22209  xkoccn  22229  alexsubALTlem2  22658  ptcmplem2  22663  tsmsfbas  22738  setsmstopn  23090  restmetu  23182  tngtopn  23261  iccntr  23431  xrge0gsumle  23443  xrge0tsms  23444  metdstri  23461  ovol0  24096  0mbl  24142  itg1le  24316  itgioo  24418  limcnlp  24478  dvbsss  24502  plyssc  24792  fsumharmonic  25591  egrsubgr  27061  0grsubgr  27062  0uhgrsubgr  27063  chocnul  29107  span0  29321  chsup0  29327  ssnnssfz  30512  xrge0tsmsd  30694  ddemeas  31497  dya2iocuni  31543  oms0  31557  0elcarsg  31567  eulerpartlemt  31631  bnj1143  32064  mrsubrn  32762  msubrn  32778  mthmpps  32831  dfpo2  32993  trpredlem1  33068  nulsslt  33264  nulssgt  33265  bj-nuliotaALT  34353  bj-restsn0  34378  bj-restsn10  34379  pibt2  34700  mblfinlem2  34932  mblfinlem3  34933  ismblfin  34935  sstotbnd2  35054  isbnd3  35064  ssbnd  35068  heiborlem6  35096  lub0N  36327  glb0N  36331  0psubN  36887  padd01  36949  padd02  36950  pol0N  37047  pcl0N  37060  0psubclN  37081  mzpcompact2lem  39355  itgocn  39771  fvnonrel  39964  clcnvlem  39990  cnvrcl0  39992  cnvtrcl0  39993  0he  40135  ntrclskb  40426  gru0eld  40572  mnu0eld  40608  mnuprdlem4  40618  mnuprd  40619  founiiun0  41458  uzfissfz  41601  limcdm0  41906  cncfiooicc  42184  itgvol0  42260  ibliooicc  42263  ovn0  42855  sprssspr  43650  ssnn0ssfz  44404  setrec2fun  44802