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 2732

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 2739  df-cleq 2752  df-clel 2835  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  5265  0elpw  5320  rel0  5779  0ima  6074  dmxpss  6164  dmsnopss  6210  dfpo2  6294  on0eqel  6483  iotassuni  6508  fun0  6598  f0  6756  fvmptss  6999  fvmptss2  7013  funressn  7156  riotassuni  7410  ordsuci  7807  frxp  8124  suppssdm  8175  suppun  8182  suppss  8192  suppssov1  8195  suppssov2  8196  suppss2  8198  suppssfv  8200  oaword1  8539  oaword2  8540  omwordri  8559  oewordri  8580  oeworde  8581  nnaword1  8617  naddword1  8680  mapssfset  8852  fodomr  9126  pwdom  9127  php  9201  isinf  9235  fodomfir  9297  finsschain  9326  fipwuni  9396  fipwss  9399  wdompwdom  9550  inf3lemd  9606  inf3lem1  9607  cantnfle  9650  ttrclselem1  9704  tc0  9724  r1val1  9768  alephgeom  10085  infmap2  10219  cfub  10250  cf0  10252  cflecard  10254  cfle  10255  fin23lem16  10337  itunitc1  10422  ttukeylem6  10516  ttukeylem7  10517  canthwe  10660  wun0  10727  tsk0  10772  gruina  10827  grur1a  10828  indconst0  12254  uzssz  12908  xrsup0  13375  fzoss1  13742  fsuppmapnn0fiubex  14056  swrd00  14712  swrdlend  14723  repswswrd  14855  xptrrel  15053  relexpdmd  15117  relexprnd  15121  relexpfldd  15123  rtrclreclem4  15134  sum0  15807  fsumss  15811  fsumcvg3  15815  prod0  16030  0bits  16529  sadid1  16558  sadid2  16559  smu01lem  16575  smu01  16576  smu02  16577  lcmf0  16724  vdwmc2  17071  vdwlem13  17085  ramz2  17116  strfvss  17279  ressbasssg  17329  ressbasssOLD  17332  ress0  17335  ismred2  17687  acsfn  17747  acsfn0  17748  0ssc  17926  fullfunc  17997  fthfunc  17998  mrelatglb0  18649  cntzssv  19455  symgsssg  19594  efgsfo  19866  dprdsn  20165  lsp0  21193  lss0v  21200  lspsnat  21332  lsppratlem3  21336  lbsexg  21351  evpmss  21799  ocv0  21890  ocvz  21891  css1  21903  resspsrbas  22188  mhp0cl  22374  psr1crng  22412  psr1assa  22413  psr1tos  22414  psr1bas2  22415  vr1cl2  22418  ply1lss  22421  ply1subrg  22422  psr1plusg  22445  psr1vsca  22446  psr1mulr  22447  psr1ring  22471  psr1lmod  22473  psr1sca  22474  0opn  23129  toponsspwpw  23147  basdif0  23178  baspartn  23179  0cld  23263  ntr0  23306  cmpfi  23633  refun0  23741  xkouni  23825  xkoccn  23845  alexsubALTlem2  24274  ptcmplem2  24279  tsmsfbas  24354  setsmstopn  24704  restmetu  24796  tngtopn  24876  iccntr  25048  xrge0gsumle  25060  xrge0tsms  25061  metdstri  25078  ovol0  25721  0mbl  25767  itg1le  25941  itgioo  26043  limcnlp  26105  dvbsss  26129  plyssc  26425  fsumharmonic  27248  nulslts  28040  nulsgts  28041  bday0b  28078  madess  28131  oldssmade  28132  oldss  28135  precsexlem8  28479  bdaypw2n0bndlem  28728  bdaypw2n0bnd  28729  egrsubgr  29737  0grsubgr  29738  0uhgrsubgr  29739  chocnul  31809  span0  32023  chsup0  32029  ssnnssfz  33258  xrge0tsmsd  33513  elrgspnlem4  33685  unitprodclb  33822  constrfiss  34261  ddemeas  34747  dya2iocuni  34794  oms0  34808  0elcarsg  34818  eulerpartlemt  34882  bnj1143  35299  rankscottu  35636  rankkardu  35697  mrsubrn  36092  msubrn  36108  mthmpps  36161  nmulss1  36794  bj-nuliotaALT  37802  bj-restsn0  37835  bj-restsn10  37836  bj-imdirco  37942  pibt2  38171  mblfinlem2  38407  mblfinlem3  38408  ismblfin  38410  sstotbnd2  38524  isbnd3  38534  ssbnd  38538  heiborlem6  38566  lub0N  40062  glb0N  40066  0psubN  40622  padd01  40684  padd02  40685  pol0N  40782  pcl0N  40795  0psubclN  40816  mzpcompact2lem  43596  itgocn  44005  oaabsb  44135  oege1  44147  nnoeomeqom  44153  cantnfresb  44165  omabs2  44173  omcl2  44174  tfsconcatb0  44185  nadd2rabex  44227  fpwfvss  44252  nla0002  44264  nla0003  44265  nla0001  44266  fvnonrel  44437  clcnvlem  44463  cnvrcl0  44465  cnvtrcl0  44466  0he  44622  ntrclskb  44909  gru0eld  45067  mnu0eld  45089  mnuprdlem4  45099  mnuprd  45100  founiiun0  46022  uzfissfz  46156  limcdm0  46448  cncfiooicc  46722  itgvol0  46796  ibliooicc  46799  ovn0  47394  sprssspr  48381  isubgr0uhgr  48789  ssnn0ssfz  49279  ipolub0  49918  ipoglb0  49920  discsubc  49990  iinfconstbas  49992  nelsubclem  49993  setc1onsubc  50528  setrec2fun  50618  setrec2mpt  50623