Theorem 0ss 4382

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

Syntax hints:   ∈ wcel 2107   ⊆ wss 3933  ∅c0 4315

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1542  df-fal 1552  df-ex 1779  df-sb 2064  df-clab 2713  df-cleq 2726  df-clel 2808  df-dif 3936  df-ss 3950  df-nul 4316

This theorem is referenced by:  ss0b  4383  0pss  4429  npss0  4430  ssdifeq0  4469  pwpw0  4795  sssn  4808  sspr  4817  sstp  4818  uni0  4917  int0el  4961  0disj  5118  disjx0  5120  tr0  5254  al0ssb  5290  0elpw  5338  rel0  5791  0ima  6078  dmxpss  6173  dmsnopss  6216  dfpo2  6298  on0eqel  6489  iotassuni  6514  iotassuniOLD  6521  fun0  6612  f0  6770  fvmptss  7009  fvmptss2  7023  funressn  7160  riotassuni  7411  ordsuci  7811  frxp  8134  suppssdm  8185  suppun  8192  suppss  8202  suppssov1  8205  suppssov2  8206  suppss2  8208  suppssfv  8210  oaword1  8573  oaword2  8574  omwordri  8593  oewordri  8613  oeworde  8614  nnaword1  8650  naddword1  8712  mapssfset  8874  0domgOLD  9124  fodomr  9151  pwdom  9152  php  9230  phpOLD  9242  isinf  9279  isinfOLD  9280  fodomfir  9351  finsschain  9382  fipwuni  9449  fipwss  9452  wdompwdom  9601  inf3lemd  9650  inf3lem1  9651  cantnfle  9694  ttrclselem1  9748  tc0  9770  r1val1  9809  alephgeom  10105  infmap2  10240  cfub  10272  cf0  10274  cflecard  10276  cfle  10277  fin23lem16  10358  itunitc1  10443  ttukeylem6  10537  ttukeylem7  10538  canthwe  10674  wun0  10741  tsk0  10786  gruina  10841  grur1a  10842  uzssz  12882  xrsup0  13348  fzoss1  13709  fsuppmapnn0fiubex  14016  swrd00  14665  swrdlend  14674  repswswrd  14805  xptrrel  15002  relexpdmd  15066  relexprnd  15070  relexpfldd  15072  rtrclreclem4  15083  sum0  15740  fsumss  15744  fsumcvg3  15748  prod0  15962  0bits  16459  sadid1  16488  sadid2  16489  smu01lem  16505  smu01  16506  smu02  16507  lcmf0  16654  vdwmc2  17000  vdwlem13  17014  ramz2  17045  strfvss  17207  ressbasssg  17264  ressbasssOLD  17267  ress0  17270  ismred2  17622  acsfn  17678  acsfn0  17679  0ssc  17858  fullfunc  17929  fthfunc  17930  mrelatglb0  18580  cntzssv  19320  symgsssg  19458  efgsfo  19730  dprdsn  20029  lsp0  20980  lss0v  20988  lspsnat  21120  lsppratlem3  21124  lbsexg  21139  evpmss  21571  ocv0  21662  ocvz  21663  css1  21675  resspsrbas  21961  mhp0cl  22117  psr1crng  22155  psr1assa  22156  psr1tos  22157  psr1bas2  22158  vr1cl2  22161  ply1lss  22165  ply1subrg  22166  psr1plusg  22189  psr1vsca  22190  psr1mulr  22191  psr1ring  22215  psr1lmod  22217  psr1sca  22218  0opn  22877  toponsspwpw  22895  basdif0  22926  baspartn  22927  0cld  23011  ntr0  23054  cmpfi  23381  refun0  23488  xkouni  23572  xkoccn  23592  alexsubALTlem2  24021  ptcmplem2  24026  tsmsfbas  24101  setsmstopn  24454  restmetu  24546  tngtopn  24626  iccntr  24798  xrge0gsumle  24810  xrge0tsms  24811  metdstri  24828  ovol0  25483  0mbl  25529  itg1le  25703  itgioo  25806  limcnlp  25868  dvbsss  25892  plyssc  26194  fsumharmonic  27010  nulsslt  27797  nulssgt  27798  bday0b  27830  madess  27870  oldssmade  27871  precsexlem8  28193  pw2bday  28373  egrsubgr  29241  0grsubgr  29242  0uhgrsubgr  29243  chocnul  31294  span0  31508  chsup0  31514  ssnnssfz  32736  xrge0tsmsd  33011  elrgspnlem4  33195  unitprodclb  33358  ddemeas  34178  dya2iocuni  34226  oms0  34240  0elcarsg  34250  eulerpartlemt  34314  bnj1143  34745  mrsubrn  35459  msubrn  35475  mthmpps  35528  bj-nuliotaALT  37000  bj-restsn0  37027  bj-restsn10  37028  bj-imdirco  37132  pibt2  37359  mblfinlem2  37606  mblfinlem3  37607  ismblfin  37609  sstotbnd2  37722  isbnd3  37732  ssbnd  37736  heiborlem6  37764  lub0N  39131  glb0N  39135  0psubN  39692  padd01  39754  padd02  39755  pol0N  39852  pcl0N  39865  0psubclN  39886  mzpcompact2lem  42707  itgocn  43121  oaabsb  43252  oege1  43264  nnoeomeqom  43270  cantnfresb  43282  omabs2  43290  omcl2  43291  tfsconcatb0  43302  nadd2rabex  43344  fpwfvss  43370  nla0002  43382  nla0003  43383  nla0001  43384  fvnonrel  43555  clcnvlem  43581  cnvrcl0  43583  cnvtrcl0  43584  0he  43740  ntrclskb  44027  gru0eld  44193  mnu0eld  44229  mnuprdlem4  44239  mnuprd  44240  founiiun0  45140  uzfissfz  45282  limcdm0  45578  cncfiooicc  45854  itgvol0  45928  ibliooicc  45931  ovn0  46526  sprssspr  47414  isubgr0uhgr  47805  ssnn0ssfz  48211  ipolub0  48837  ipoglb0  48839  setrec2fun  49207  setrec2mpt  49212