Theorem 0ss 4423

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

Syntax hints:   ∈ wcel 2108   ⊆ wss 3976  ∅c0 4352

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-dif 3979  df-ss 3993  df-nul 4353

This theorem is referenced by:  ss0b  4424  0pss  4470  npss0  4471  ssdifeq0  4510  pwpw0  4838  sssn  4851  sspr  4860  sstp  4861  uni0  4959  int0el  5003  0disj  5159  disjx0  5161  tr0  5296  al0ssb  5326  0elpw  5374  rel0  5823  0ima  6107  dmxpss  6202  dmsnopss  6245  dfpo2  6327  on0eqel  6519  iotassuni  6545  iotassuniOLD  6552  fun0  6643  f0  6802  fvmptss  7041  fvmptss2  7055  funressn  7193  riotassuni  7445  ordsuci  7844  frxp  8167  suppssdm  8218  suppun  8225  suppss  8235  suppssov1  8238  suppssov2  8239  suppss2  8241  suppssfv  8243  oaword1  8608  oaword2  8609  omwordri  8628  oewordri  8648  oeworde  8649  nnaword1  8685  naddword1  8747  mapssfset  8909  0domgOLD  9167  fodomr  9194  pwdom  9195  php  9273  phpOLD  9285  isinf  9323  isinfOLD  9324  fodomfir  9396  finsschain  9429  fipwuni  9495  fipwss  9498  wdompwdom  9647  inf3lemd  9696  inf3lem1  9697  cantnfle  9740  ttrclselem1  9794  tc0  9816  r1val1  9855  alephgeom  10151  infmap2  10286  cfub  10318  cf0  10320  cflecard  10322  cfle  10323  fin23lem16  10404  itunitc1  10489  ttukeylem6  10583  ttukeylem7  10584  canthwe  10720  wun0  10787  tsk0  10832  gruina  10887  grur1a  10888  uzssz  12924  xrsup0  13385  fzoss1  13743  fsuppmapnn0fiubex  14043  swrd00  14692  swrdlend  14701  repswswrd  14832  xptrrel  15029  relexpdmd  15093  relexprnd  15097  relexpfldd  15099  rtrclreclem4  15110  sum0  15769  fsumss  15773  fsumcvg3  15777  prod0  15991  0bits  16485  sadid1  16514  sadid2  16515  smu01lem  16531  smu01  16532  smu02  16533  lcmf0  16681  vdwmc2  17026  vdwlem13  17040  ramz2  17071  strfvss  17234  ressbasssg  17295  ressbasssOLD  17298  ress0  17302  ismred2  17661  acsfn  17717  acsfn0  17718  0ssc  17901  fullfunc  17973  fthfunc  17974  mrelatglb0  18631  cntzssv  19368  symgsssg  19509  efgsfo  19781  dprdsn  20080  lsp0  21030  lss0v  21038  lspsnat  21170  lsppratlem3  21174  lbsexg  21189  evpmss  21627  ocv0  21718  ocvz  21719  css1  21731  resspsrbas  22017  mhp0cl  22173  psr1crng  22209  psr1assa  22210  psr1tos  22211  psr1bas2  22212  vr1cl2  22215  ply1lss  22219  ply1subrg  22220  psr1plusg  22243  psr1vsca  22244  psr1mulr  22245  psr1ring  22269  psr1lmod  22271  psr1sca  22272  0opn  22931  toponsspwpw  22949  basdif0  22981  baspartn  22982  0cld  23067  ntr0  23110  cmpfi  23437  refun0  23544  xkouni  23628  xkoccn  23648  alexsubALTlem2  24077  ptcmplem2  24082  tsmsfbas  24157  setsmstopn  24511  restmetu  24604  tngtopn  24692  iccntr  24862  xrge0gsumle  24874  xrge0tsms  24875  metdstri  24892  ovol0  25547  0mbl  25593  itg1le  25768  itgioo  25871  limcnlp  25933  dvbsss  25957  plyssc  26259  fsumharmonic  27073  nulsslt  27860  nulssgt  27861  bday0b  27893  madess  27933  oldssmade  27934  precsexlem8  28256  pw2bday  28436  egrsubgr  29312  0grsubgr  29313  0uhgrsubgr  29314  chocnul  31360  span0  31574  chsup0  31580  ssnnssfz  32792  xrge0tsmsd  33041  unitprodclb  33382  ddemeas  34200  dya2iocuni  34248  oms0  34262  0elcarsg  34272  eulerpartlemt  34336  bnj1143  34766  mrsubrn  35481  msubrn  35497  mthmpps  35550  bj-nuliotaALT  37024  bj-restsn0  37051  bj-restsn10  37052  bj-imdirco  37156  pibt2  37383  mblfinlem2  37618  mblfinlem3  37619  ismblfin  37621  sstotbnd2  37734  isbnd3  37744  ssbnd  37748  heiborlem6  37776  lub0N  39145  glb0N  39149  0psubN  39706  padd01  39768  padd02  39769  pol0N  39866  pcl0N  39879  0psubclN  39900  mzpcompact2lem  42707  itgocn  43121  oaabsb  43256  oege1  43268  nnoeomeqom  43274  cantnfresb  43286  omabs2  43294  omcl2  43295  tfsconcatb0  43306  nadd2rabex  43348  fpwfvss  43374  nla0002  43386  nla0003  43387  nla0001  43388  fvnonrel  43559  clcnvlem  43585  cnvrcl0  43587  cnvtrcl0  43588  0he  43744  ntrclskb  44031  gru0eld  44198  mnu0eld  44234  mnuprdlem4  44244  mnuprd  44245  founiiun0  45097  uzfissfz  45241  limcdm0  45539  cncfiooicc  45815  itgvol0  45889  ibliooicc  45892  ovn0  46487  sprssspr  47355  isubgr0uhgr  47743  ssnn0ssfz  48074  ipolub0  48664  ipoglb0  48666  setrec2fun  48784  setrec2mpt  48789