Theorem 0ss 4357

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

Syntax hints:   ∈ wcel 2145   ⊆ wss 3907  ∅c0 4288

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1566  df-fal 1576  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-dif 3910  df-ss 3924  df-nul 4289

This theorem is referenced by:  ss0b  4358  0pss  4404  npss0  4405  ssdifeq0  4443  pwpw0  4774  sssn  4787  sspr  4795  sstp  4796  uni0OLD  4897  int0el  4939  0disj  5097  disjx0  5099  tr0  5224  al0ssb  5262  0elpw  5316  rel0  5775  0ima  6070  dmxpss  6160  dmsnopss  6204  dfpo2  6286  on0eqel  6475  iotassuni  6500  fun0  6590  f0  6749  fvmptss  6992  fvmptss2  7006  funressn  7146  riotassuni  7397  ordsuci  7795  frxp  8110  suppssdm  8161  suppun  8168  suppss  8178  suppssov1  8181  suppssov2  8182  suppss2  8184  suppssfv  8186  oaword1  8525  oaword2  8526  omwordri  8545  oewordri  8566  oeworde  8567  nnaword1  8603  naddword1  8666  mapssfset  8836  fodomr  9104  pwdom  9105  php  9179  isinf  9213  fodomfir  9275  finsschain  9304  fipwuni  9374  fipwss  9377  wdompwdom  9528  inf3lemd  9584  inf3lem1  9585  cantnfle  9628  ttrclselem1  9682  tc0  9702  r1val1  9746  alephgeom  10054  infmap2  10188  cfub  10220  cf0  10222  cflecard  10224  cfle  10225  fin23lem16  10307  itunitc1  10392  ttukeylem6  10486  ttukeylem7  10487  canthwe  10624  wun0  10691  tsk0  10736  gruina  10791  grur1a  10792  indconst0  12218  uzssz  12871  xrsup0  13337  fzoss1  13703  fsuppmapnn0fiubex  14016  swrd00  14670  swrdlend  14679  repswswrd  14809  xptrrel  15005  relexpdmd  15069  relexprnd  15073  relexpfldd  15075  rtrclreclem4  15086  sum0  15760  fsumss  15764  fsumcvg3  15768  prod0  15985  0bits  16485  sadid1  16514  sadid2  16515  smu01lem  16531  smu01  16532  smu02  16533  lcmf0  16680  vdwmc2  17027  vdwlem13  17041  ramz2  17072  strfvss  17235  ressbasssg  17285  ressbasssOLD  17288  ress0  17291  ismred2  17643  acsfn  17703  acsfn0  17704  0ssc  17882  fullfunc  17953  fthfunc  17954  mrelatglb0  18605  cntzssv  19386  symgsssg  19525  efgsfo  19797  dprdsn  20096  lsp0  21096  lss0v  21103  lspsnat  21235  lsppratlem3  21239  lbsexg  21254  evpmss  21693  ocv0  21784  ocvz  21785  css1  21797  resspsrbas  22080  mhp0cl  22266  psr1crng  22304  psr1assa  22305  psr1tos  22306  psr1bas2  22307  vr1cl2  22310  ply1lss  22313  ply1subrg  22314  psr1plusg  22337  psr1vsca  22338  psr1mulr  22339  psr1ring  22363  psr1lmod  22365  psr1sca  22366  0opn  23018  toponsspwpw  23036  basdif0  23067  baspartn  23068  0cld  23152  ntr0  23195  cmpfi  23522  refun0  23629  xkouni  23713  xkoccn  23733  alexsubALTlem2  24162  ptcmplem2  24167  tsmsfbas  24242  setsmstopn  24592  restmetu  24684  tngtopn  24764  iccntr  24936  xrge0gsumle  24948  xrge0tsms  24949  metdstri  24966  ovol0  25609  0mbl  25655  itg1le  25829  itgioo  25932  limcnlp  25994  dvbsss  26018  plyssc  26314  fsumharmonic  27130  nulslts  27922  nulsgts  27923  bday0b  27960  madess  28013  oldssmade  28014  oldss  28017  precsexlem8  28361  bdaypw2n0bndlem  28610  bdaypw2n0bnd  28611  egrsubgr  29532  0grsubgr  29533  0uhgrsubgr  29534  chocnul  31585  span0  31799  chsup0  31805  ssnnssfz  33040  xrge0tsmsd  33301  elrgspnlem4  33473  unitprodclb  33613  constrfiss  34053  ddemeas  34538  dya2iocuni  34585  oms0  34599  0elcarsg  34609  eulerpartlemt  34673  bnj1143  35090  mrsubrn  35871  msubrn  35887  mthmpps  35940  bj-nuliotaALT  37550  bj-restsn0  37582  bj-restsn10  37583  bj-imdirco  37689  pibt2  37918  mblfinlem2  38164  mblfinlem3  38165  ismblfin  38167  sstotbnd2  38280  isbnd3  38290  ssbnd  38294  heiborlem6  38322  lub0N  39820  glb0N  39824  0psubN  40380  padd01  40442  padd02  40443  pol0N  40540  pcl0N  40553  0psubclN  40574  mzpcompact2lem  43339  itgocn  43748  oaabsb  43878  oege1  43890  nnoeomeqom  43896  cantnfresb  43908  omabs2  43916  omcl2  43917  tfsconcatb0  43928  nadd2rabex  43970  fpwfvss  43995  nla0002  44007  nla0003  44008  nla0001  44009  fvnonrel  44180  clcnvlem  44206  cnvrcl0  44208  cnvtrcl0  44209  0he  44365  ntrclskb  44652  gru0eld  44812  mnu0eld  44834  mnuprdlem4  44844  mnuprd  44845  founiiun0  45767  uzfissfz  45901  limcdm0  46193  cncfiooicc  46467  itgvol0  46541  ibliooicc  46544  ovn0  47139  sprssspr  48086  isubgr0uhgr  48494  ssnn0ssfz  48981  ipolub0  49622  ipoglb0  49624  discsubc  49694  iinfconstbas  49696  nelsubclem  49697  setc1onsubc  50232  setrec2fun  50322  setrec2mpt  50327