Theorem 0ss 4350

Description: The empty set is a subset of any class. Dual of ssv 3955. 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 4284	. . 3 ⊢ ¬ 𝑥 ∈ ∅
2	1	pm2.21i 120	. 2 ⊢ (𝑥 ∈ ∅ → 𝑥 ∈ 𝐴)
3	2	ssriv 3935	1 ⊢ ∅ ⊆ 𝐴

This proof depends on syntax axioms:   ∈ wcel 2145   ⊆ wss 3899  ∅c0 4279

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-dif 3902  df-ss 3916  df-nul 4280

This theorem is used by:  ss0b  4351  0pss  4360  npss0  4361  ssdifeq0  4442  pwpw0  4774  sssn  4787  sspr  4795  sstp  4796  uni0OLD  4897  int0el  4939  0disj  5096  disjx0  5098  tr0  5225  al0ssb  5262  0elpw  5317  rel0  5776  dmxpss  6163  0ima  6200  dmsnopss  6215  dfpo2  6299  on0eqel  6488  iotassuni  6513  fun0  6605  f0  6763  fvmptss  7006  fvmptss2  7020  funressn  7163  riotassuni  7417  ordsuci  7822  frxp  8138  suppssdm  8194  suppun  8201  suppss  8211  suppssov1  8214  suppssov2  8215  suppss2  8217  suppssfv  8219  oaword1  8560  oaword2  8561  omwordri  8580  oewordri  8601  oeworde  8602  nnaword1  8638  naddword1  8701  mapssfset  8873  fodomr  9147  pwdom  9148  php  9222  isinf  9256  fodomfir  9319  finsschain  9348  fipwuni  9418  fipwss  9421  wdompwdom  9572  inf3lemd  9628  inf3lem1  9629  cantnfle  9672  ttrclselem1  9726  tc0  9746  r1val1  9793  setrec2fun  9973  alephgeom  10161  infmap2  10295  cfub  10326  cf0  10328  cflecard  10330  cfle  10331  fin23lem16  10413  itunitc1  10498  ttukeylem6  10592  ttukeylem7  10593  canthwe  10736  wun0  10803  tsk0  10848  gruina  10903  grur1a  10904  indconst0  12332  uzssz  12986  xrsup0  13453  fzoss1  13821  fsuppmapnn0fiubex  14135  swrd00  14792  swrdlend  14803  repswswrd  14935  xptrrel  15133  relexpdmd  15197  relexprnd  15201  relexpfldd  15203  rtrclreclem4  15214  sum0  15887  fsumss  15891  fsumcvg3  15895  prod0  16110  0bits  16609  sadid1  16638  sadid2  16639  smu01lem  16655  smu01  16656  smu02  16657  lcmf0  16809  vdwmc2  17157  vdwlem13  17171  ramz2  17202  strfvss  17365  ressbasssg  17415  ressbasssOLD  17418  ress0  17421  ismred2  17773  acsfn  17833  acsfn0  17834  0ssc  18012  fullfunc  18083  fthfunc  18084  mrelatglb0  18735  cntzssv  19542  symgsssg  19681  efgsfo  19953  dprdsn  20252  lsp0  21284  lss0v  21291  lspsnat  21423  lsppratlem3  21427  lbsexg  21442  evpmss  21892  ocv0  21983  ocvz  21984  css1  21996  resspsrbas  22281  mhp0cl  22467  psr1crng  22505  psr1assa  22506  psr1tos  22507  psr1bas2  22508  vr1cl2  22511  ply1lss  22514  ply1subrg  22515  psr1plusg  22538  psr1vsca  22539  psr1mulr  22540  psr1ring  22564  psr1lmod  22566  psr1sca  22567  0opn  23222  toponsspwpw  23240  basdif0  23271  baspartn  23272  0cld  23356  ntr0  23399  cmpfi  23726  refun0  23834  xkouni  23918  xkoccn  23938  alexsubALTlem2  24367  ptcmplem2  24372  tsmsfbas  24447  setsmstopn  24797  restmetu  24889  tngtopn  24969  iccntr  25141  xrge0gsumle  25153  xrge0tsms  25154  metdstri  25171  ovol0  25814  0mbl  25860  itg1le  26034  itgioo  26136  limcnlp  26198  dvbsss  26222  plyssc  26518  fsumharmonic  27339  nulslts  28161  nulsgts  28162  bday0b  28199  madess  28252  oldssmade  28253  oldss  28256  precsexlem8  28600  bdaypw2n0bndlem  28849  bdaypw2n0bnd  28850  egrsubgr  29858  0grsubgr  29859  0uhgrsubgr  29860  chocnul  31930  span0  32144  chsup0  32150  ssnnssfz  33379  xrge0tsmsd  33634  elrgspnlem4  33806  unitprodclb  33944  constrfiss  34383  ddemeas  34869  dya2iocuni  34915  oms0  34929  0elcarsg  34939  eulerpartlemt  35003  bnj1143  35420  rankscottu  35753  rankkardu  35839  mrsubrn  36278  msubrn  36294  mthmpps  36347  nmulss1  36963  bj-nuliotaALT  37973  bj-restsn0  38006  bj-restsn10  38007  bj-imdirco  38111  pibt2  38340  mblfinlem2  38576  mblfinlem3  38577  ismblfin  38579  varprop  38642  sstotbnd2  38708  isbnd3  38718  ssbnd  38722  heiborlem6  38750  lub0N  40246  glb0N  40250  0psubN  40806  padd01  40868  padd02  40869  pol0N  40966  pcl0N  40979  0psubclN  41000  mzpcompact2lem  43761  itgocn  44165  oaabsb  44295  oege1  44307  nnoeomeqom  44313  cantnfresb  44325  omabs2  44333  omcl2  44334  tfsconcatb0  44345  nadd2rabex  44387  fpwfvss  44412  nla0002  44424  nla0003  44425  nla0001  44426  fvnonrel  44596  clcnvlem  44622  cnvrcl0  44624  cnvtrcl0  44625  0he  44781  ntrclskb  45068  gru0eld  45226  mnu0eld  45248  mnuprdlem4  45258  mnuprd  45259  founiiun0  46204  uzfissfz  46337  limcdm0  46629  cncfiooicc  46903  itgvol0  46977  ibliooicc  46980  ovn0  47575  sprssspr  48562  isubgr0uhgr  48970  ssnn0ssfz  49460  ipolub0  50099  ipoglb0  50101  discsubc  50171  iinfconstbas  50173  nelsubclem  50174  setc1onsubc  50709  setrec2mpt  50789