Theorem 0ss 4357

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

This proof depends on syntax axioms:   ∈ wcel 2146   ⊆ wss 3906  ∅c0 4286

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 2148  ax-9 2156  ax-ext 2737

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 2744  df-cleq 2757  df-clel 2840  df-dif 3909  df-ss 3923  df-nul 4287

This theorem is used by:  ss0b  4358  0pss  4367  npss0  4368  ssdifeq0  4449  pwpw0  4781  sssn  4794  sspr  4802  sstp  4803  uni0OLD  4904  int0el  4946  0disj  5104  disjx0  5106  tr0  5233  al0ssb  5273  0elpw  5328  rel0  5787  0ima  6082  dmxpss  6171  dmsnopss  6217  dfpo2  6301  on0eqel  6490  iotassuni  6515  fun0  6605  f0  6763  fvmptss  7006  fvmptss2  7020  funressn  7160  riotassuni  7413  ordsuci  7809  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  8850  fodomr  9119  pwdom  9120  php  9194  isinf  9228  fodomfir  9290  finsschain  9319  fipwuni  9389  fipwss  9392  wdompwdom  9543  inf3lemd  9599  inf3lem1  9600  cantnfle  9643  ttrclselem1  9697  tc0  9717  r1val1  9761  alephgeom  10078  infmap2  10212  cfub  10243  cf0  10245  cflecard  10247  cfle  10248  fin23lem16  10330  itunitc1  10415  ttukeylem6  10509  ttukeylem7  10510  canthwe  10647  wun0  10714  tsk0  10759  gruina  10814  grur1a  10815  indconst0  12241  uzssz  12894  xrsup0  13360  fzoss1  13727  fsuppmapnn0fiubex  14041  swrd00  14697  swrdlend  14708  repswswrd  14840  xptrrel  15036  relexpdmd  15100  relexprnd  15104  relexpfldd  15106  rtrclreclem4  15117  sum0  15790  fsumss  15794  fsumcvg3  15798  prod0  16015  0bits  16514  sadid1  16543  sadid2  16544  smu01lem  16560  smu01  16561  smu02  16562  lcmf0  16709  vdwmc2  17056  vdwlem13  17070  ramz2  17101  strfvss  17264  ressbasssg  17314  ressbasssOLD  17317  ress0  17320  ismred2  17672  acsfn  17732  acsfn0  17733  0ssc  17911  fullfunc  17982  fthfunc  17983  mrelatglb0  18634  cntzssv  19421  symgsssg  19560  efgsfo  19832  dprdsn  20131  lsp0  21159  lss0v  21166  lspsnat  21298  lsppratlem3  21302  lbsexg  21317  evpmss  21765  ocv0  21856  ocvz  21857  css1  21869  resspsrbas  22152  mhp0cl  22338  psr1crng  22376  psr1assa  22377  psr1tos  22378  psr1bas2  22379  vr1cl2  22382  ply1lss  22385  ply1subrg  22386  psr1plusg  22409  psr1vsca  22410  psr1mulr  22411  psr1ring  22435  psr1lmod  22437  psr1sca  22438  0opn  23090  toponsspwpw  23108  basdif0  23139  baspartn  23140  0cld  23224  ntr0  23267  cmpfi  23594  refun0  23701  xkouni  23785  xkoccn  23805  alexsubALTlem2  24234  ptcmplem2  24239  tsmsfbas  24314  setsmstopn  24664  restmetu  24756  tngtopn  24836  iccntr  25008  xrge0gsumle  25020  xrge0tsms  25021  metdstri  25038  ovol0  25681  0mbl  25727  itg1le  25901  itgioo  26004  limcnlp  26066  dvbsss  26090  plyssc  26386  fsumharmonic  27205  nulslts  27997  nulsgts  27998  bday0b  28035  madess  28088  oldssmade  28089  oldss  28092  precsexlem8  28436  bdaypw2n0bndlem  28685  bdaypw2n0bnd  28686  egrsubgr  29656  0grsubgr  29657  0uhgrsubgr  29658  chocnul  31709  span0  31923  chsup0  31929  ssnnssfz  33161  xrge0tsmsd  33416  elrgspnlem4  33588  unitprodclb  33725  constrfiss  34164  ddemeas  34650  dya2iocuni  34697  oms0  34711  0elcarsg  34721  eulerpartlemt  34785  bnj1143  35202  rankscottu  35539  rankkardu  35600  mrsubrn  36018  msubrn  36034  mthmpps  36087  nmulss1  36719  bj-nuliotaALT  37727  bj-restsn0  37760  bj-restsn10  37761  bj-imdirco  37867  pibt2  38096  mblfinlem2  38342  mblfinlem3  38343  ismblfin  38345  sstotbnd2  38458  isbnd3  38468  ssbnd  38472  heiborlem6  38500  lub0N  39996  glb0N  40000  0psubN  40556  padd01  40618  padd02  40619  pol0N  40716  pcl0N  40729  0psubclN  40750  mzpcompact2lem  43515  itgocn  43924  oaabsb  44054  oege1  44066  nnoeomeqom  44072  cantnfresb  44084  omabs2  44092  omcl2  44093  tfsconcatb0  44104  nadd2rabex  44146  fpwfvss  44171  nla0002  44183  nla0003  44184  nla0001  44185  fvnonrel  44356  clcnvlem  44382  cnvrcl0  44384  cnvtrcl0  44385  0he  44541  ntrclskb  44828  gru0eld  44986  mnu0eld  45008  mnuprdlem4  45018  mnuprd  45019  founiiun0  45941  uzfissfz  46075  limcdm0  46367  cncfiooicc  46641  itgvol0  46715  ibliooicc  46718  ovn0  47313  sprssspr  48263  isubgr0uhgr  48671  ssnn0ssfz  49162  ipolub0  49803  ipoglb0  49805  discsubc  49875  iinfconstbas  49877  nelsubclem  49878  setc1onsubc  50413  setrec2fun  50503  setrec2mpt  50508