Theorem 0ss 4349

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

Syntax hints:   ∈ wcel 2113   ⊆ wss 3898  ∅c0 4282

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 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-dif 3901  df-ss 3915  df-nul 4283

This theorem is referenced by:  ss0b  4350  0pss  4396  npss0  4397  ssdifeq0  4436  pwpw0  4764  sssn  4777  sspr  4786  sstp  4787  uni0OLD  4887  int0el  4929  0disj  5086  disjx0  5088  tr0  5212  al0ssb  5248  0elpw  5296  rel0  5743  0ima  6031  dmxpss  6123  dmsnopss  6166  dfpo2  6248  on0eqel  6436  iotassuni  6461  fun0  6551  f0  6709  fvmptss  6947  fvmptss2  6961  funressn  7098  riotassuni  7349  ordsuci  7747  frxp  8062  suppssdm  8113  suppun  8120  suppss  8130  suppssov1  8133  suppssov2  8134  suppss2  8136  suppssfv  8138  oaword1  8473  oaword2  8474  omwordri  8493  oewordri  8513  oeworde  8514  nnaword1  8550  naddword1  8612  mapssfset  8781  fodomr  9048  pwdom  9049  php  9123  isinf  9156  fodomfir  9219  finsschain  9250  fipwuni  9317  fipwss  9320  wdompwdom  9471  inf3lemd  9524  inf3lem1  9525  cantnfle  9568  ttrclselem1  9622  tc0  9642  r1val1  9686  alephgeom  9980  infmap2  10115  cfub  10147  cf0  10149  cflecard  10151  cfle  10152  fin23lem16  10233  itunitc1  10318  ttukeylem6  10412  ttukeylem7  10413  canthwe  10549  wun0  10616  tsk0  10661  gruina  10716  grur1a  10717  uzssz  12759  xrsup0  13224  fzoss1  13588  fsuppmapnn0fiubex  13901  swrd00  14554  swrdlend  14563  repswswrd  14693  xptrrel  14889  relexpdmd  14953  relexprnd  14957  relexpfldd  14959  rtrclreclem4  14970  sum0  15630  fsumss  15634  fsumcvg3  15638  prod0  15852  0bits  16352  sadid1  16381  sadid2  16382  smu01lem  16398  smu01  16399  smu02  16400  lcmf0  16547  vdwmc2  16893  vdwlem13  16907  ramz2  16938  strfvss  17100  ressbasssg  17150  ressbasssOLD  17153  ress0  17156  ismred2  17507  acsfn  17567  acsfn0  17568  0ssc  17746  fullfunc  17817  fthfunc  17818  mrelatglb0  18469  cntzssv  19242  symgsssg  19381  efgsfo  19653  dprdsn  19952  lsp0  20944  lss0v  20952  lspsnat  21084  lsppratlem3  21088  lbsexg  21103  evpmss  21525  ocv0  21616  ocvz  21617  css1  21629  resspsrbas  21912  mhp0cl  22062  psr1crng  22100  psr1assa  22101  psr1tos  22102  psr1bas2  22103  vr1cl2  22106  ply1lss  22110  ply1subrg  22111  psr1plusg  22134  psr1vsca  22135  psr1mulr  22136  psr1ring  22160  psr1lmod  22162  psr1sca  22163  0opn  22820  toponsspwpw  22838  basdif0  22869  baspartn  22870  0cld  22954  ntr0  22997  cmpfi  23324  refun0  23431  xkouni  23515  xkoccn  23535  alexsubALTlem2  23964  ptcmplem2  23969  tsmsfbas  24044  setsmstopn  24394  restmetu  24486  tngtopn  24566  iccntr  24738  xrge0gsumle  24750  xrge0tsms  24751  metdstri  24768  ovol0  25422  0mbl  25468  itg1le  25642  itgioo  25745  limcnlp  25807  dvbsss  25831  plyssc  26133  fsumharmonic  26950  nulsslt  27739  nulssgt  27740  bday0b  27775  madess  27822  oldssmade  27823  oldss  27824  precsexlem8  28153  egrsubgr  29257  0grsubgr  29258  0uhgrsubgr  29259  chocnul  31310  span0  31524  chsup0  31530  ssnnssfz  32774  indconst0  32846  xrge0tsmsd  33049  elrgspnlem4  33219  unitprodclb  33361  constrfiss  33785  ddemeas  34270  dya2iocuni  34317  oms0  34331  0elcarsg  34341  eulerpartlemt  34405  bnj1143  34823  mrsubrn  35578  msubrn  35594  mthmpps  35647  bj-nuliotaALT  37123  bj-restsn0  37150  bj-restsn10  37151  bj-imdirco  37255  pibt2  37482  mblfinlem2  37719  mblfinlem3  37720  ismblfin  37722  sstotbnd2  37835  isbnd3  37845  ssbnd  37849  heiborlem6  37877  lub0N  39309  glb0N  39313  0psubN  39869  padd01  39931  padd02  39932  pol0N  40029  pcl0N  40042  0psubclN  40063  mzpcompact2lem  42869  itgocn  43282  oaabsb  43412  oege1  43424  nnoeomeqom  43430  cantnfresb  43442  omabs2  43450  omcl2  43451  tfsconcatb0  43462  nadd2rabex  43504  fpwfvss  43530  nla0002  43542  nla0003  43543  nla0001  43544  fvnonrel  43715  clcnvlem  43741  cnvrcl0  43743  cnvtrcl0  43744  0he  43900  ntrclskb  44187  gru0eld  44347  mnu0eld  44383  mnuprdlem4  44393  mnuprd  44394  founiiun0  45312  uzfissfz  45450  limcdm0  45743  cncfiooicc  46017  itgvol0  46091  ibliooicc  46094  ovn0  46689  sprssspr  47606  isubgr0uhgr  47998  ssnn0ssfz  48474  ipolub0  49117  ipoglb0  49119  discsubc  49190  iinfconstbas  49192  nelsubclem  49193  setc1onsubc  49728  setrec2fun  49818  setrec2mpt  49823