Theorem 0ss 4335

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

Syntax hints:   ∈ wcel 2119   ⊆ wss 3890  ∅c0 4268

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-dif 3893  df-ss 3907  df-nul 4269

This theorem is referenced by:  ss0b  4336  0pss  4382  npss0  4383  ssdifeq0  4421  pwpw0  4751  sssn  4764  sspr  4773  sstp  4774  uni0OLD  4874  int0el  4916  0disj  5072  disjx0  5074  tr0  5199  al0ssb  5237  0elpw  5291  rel0  5749  0ima  6037  dmxpss  6129  dmsnopss  6172  dfpo2  6254  on0eqel  6442  iotassuni  6467  fun0  6557  f0  6715  fvmptss  6955  fvmptss2  6969  funressn  7109  riotassuni  7360  ordsuci  7758  frxp  8073  suppssdm  8124  suppun  8131  suppss  8141  suppssov1  8144  suppssov2  8145  suppss2  8147  suppssfv  8149  oaword1  8484  oaword2  8485  omwordri  8504  oewordri  8525  oeworde  8526  nnaword1  8562  naddword1  8624  mapssfset  8795  fodomr  9063  pwdom  9064  php  9138  isinf  9172  fodomfir  9235  finsschain  9266  fipwuni  9336  fipwss  9339  wdompwdom  9490  inf3lemd  9546  inf3lem1  9547  cantnfle  9590  ttrclselem1  9644  tc0  9664  r1val1  9708  alephgeom  10002  infmap2  10137  cfub  10169  cf0  10171  cflecard  10173  cfle  10174  fin23lem16  10255  itunitc1  10340  ttukeylem6  10434  ttukeylem7  10435  canthwe  10572  wun0  10639  tsk0  10684  gruina  10739  grur1a  10740  indconst0  12169  uzssz  12807  xrsup0  13273  fzoss1  13639  fsuppmapnn0fiubex  13952  swrd00  14605  swrdlend  14614  repswswrd  14744  xptrrel  14940  relexpdmd  15004  relexprnd  15008  relexpfldd  15010  rtrclreclem4  15021  sum0  15681  fsumss  15685  fsumcvg3  15689  prod0  15906  0bits  16406  sadid1  16435  sadid2  16436  smu01lem  16452  smu01  16453  smu02  16454  lcmf0  16601  vdwmc2  16948  vdwlem13  16962  ramz2  16993  strfvss  17155  ressbasssg  17205  ressbasssOLD  17208  ress0  17211  ismred2  17563  acsfn  17623  acsfn0  17624  0ssc  17802  fullfunc  17873  fthfunc  17874  mrelatglb0  18525  cntzssv  19301  symgsssg  19440  efgsfo  19712  dprdsn  20011  lsp0  21006  lss0v  21013  lspsnat  21145  lsppratlem3  21149  lbsexg  21164  evpmss  21568  ocv0  21659  ocvz  21660  css1  21672  resspsrbas  21955  mhp0cl  22141  psr1crng  22179  psr1assa  22180  psr1tos  22181  psr1bas2  22182  vr1cl2  22185  ply1lss  22188  ply1subrg  22189  psr1plusg  22212  psr1vsca  22213  psr1mulr  22214  psr1ring  22238  psr1lmod  22240  psr1sca  22241  0opn  22894  toponsspwpw  22912  basdif0  22943  baspartn  22944  0cld  23028  ntr0  23071  cmpfi  23398  refun0  23505  xkouni  23589  xkoccn  23609  alexsubALTlem2  24038  ptcmplem2  24043  tsmsfbas  24118  setsmstopn  24468  restmetu  24560  tngtopn  24640  iccntr  24812  xrge0gsumle  24824  xrge0tsms  24825  metdstri  24842  ovol0  25485  0mbl  25531  itg1le  25705  itgioo  25808  limcnlp  25870  dvbsss  25894  plyssc  26190  fsumharmonic  27000  nulslts  27792  nulsgts  27793  bday0b  27830  madess  27883  oldssmade  27884  oldss  27887  precsexlem8  28231  bdaypw2n0bndlem  28480  bdaypw2n0bnd  28481  egrsubgr  29371  0grsubgr  29372  0uhgrsubgr  29373  chocnul  31424  span0  31638  chsup0  31644  ssnnssfz  32886  xrge0tsmsd  33161  elrgspnlem4  33333  unitprodclb  33479  constrfiss  33942  ddemeas  34427  dya2iocuni  34474  oms0  34488  0elcarsg  34498  eulerpartlemt  34562  bnj1143  34979  mrsubrn  35748  msubrn  35764  mthmpps  35817  bj-nuliotaALT  37418  bj-restsn0  37450  bj-restsn10  37451  bj-imdirco  37557  pibt2  37786  mblfinlem2  38032  mblfinlem3  38033  ismblfin  38035  sstotbnd2  38148  isbnd3  38158  ssbnd  38162  heiborlem6  38190  lub0N  39688  glb0N  39692  0psubN  40248  padd01  40310  padd02  40311  pol0N  40408  pcl0N  40421  0psubclN  40442  mzpcompact2lem  43207  itgocn  43616  oaabsb  43746  oege1  43758  nnoeomeqom  43764  cantnfresb  43776  omabs2  43784  omcl2  43785  tfsconcatb0  43796  nadd2rabex  43838  fpwfvss  43863  nla0002  43875  nla0003  43876  nla0001  43877  fvnonrel  44048  clcnvlem  44074  cnvrcl0  44076  cnvtrcl0  44077  0he  44233  ntrclskb  44520  gru0eld  44680  mnu0eld  44716  mnuprdlem4  44726  mnuprd  44727  founiiun0  45644  uzfissfz  45778  limcdm0  46070  cncfiooicc  46344  itgvol0  46418  ibliooicc  46421  ovn0  47016  sprssspr  47963  isubgr0uhgr  48371  ssnn0ssfz  48847  ipolub0  49489  ipoglb0  49491  discsubc  49561  iinfconstbas  49563  nelsubclem  49564  setc1onsubc  50099  setrec2fun  50189  setrec2mpt  50194