Theorem 0ss 4197

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

Syntax hints:   ∈ wcel 2164   ⊆ wss 3798  ∅c0 4144

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009  ax-6 2075  ax-7 2112  ax-9 2173  ax-10 2192  ax-11 2207  ax-12 2220  ax-ext 2803

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 879  df-tru 1660  df-ex 1879  df-nf 1883  df-sb 2068  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-v 3416  df-dif 3801  df-in 3805  df-ss 3812  df-nul 4145

This theorem is referenced by:  ss0b  4198  0pss  4238  npss0  4239  ssdifeq0  4274  pwpw0  4562  sssn  4575  sspr  4582  sstp  4583  pwsnALT  4651  uni0  4687  int0el  4728  0disj  4866  disjx0  4868  tr0  4986  al0ssb  5015  0elpw  5056  rel0  5457  0ima  5723  dmxpss  5806  dmsnopss  5848  on0eqel  6080  iotassuni  6102  fun0  6187  fresaunres2  6313  f0  6323  fvmptss  6539  fvmptss2  6552  funressn  6677  riotassuni  6903  frxp  7551  suppssdm  7572  suppun  7579  suppss  7590  suppssov1  7592  suppss2  7594  suppssfv  7596  oaword1  7899  oaword2  7900  omwordri  7919  oewordri  7939  oeworde  7940  nnaword1  7976  0domg  8356  fodomr  8380  pwdom  8381  php  8413  isinf  8442  finsschain  8542  fipwuni  8601  fipwss  8604  wdompwdom  8752  inf3lemd  8801  inf3lem1  8802  cantnfle  8845  tc0  8900  r1val1  8926  alephgeom  9218  infmap2  9355  cfub  9386  cf0  9388  cflecard  9390  cfle  9391  fin23lem16  9472  itunitc1  9557  ttukeylem6  9651  ttukeylem7  9652  canthwe  9788  wun0  9855  tsk0  9900  gruina  9955  grur1a  9956  uzssz  11988  xrsup0  12441  fzoss1  12790  fsuppmapnn0fiubex  13086  swrd00  13704  swrdlend  13718  swrd0  13723  repswswrd  13900  xptrrel  14098  sum0  14829  fsumss  14833  fsumcvg3  14837  prod0  15046  0bits  15534  sadid1  15563  sadid2  15564  smu01lem  15580  smu01  15581  smu02  15582  lcmf0  15720  vdwmc2  16054  vdwlem13  16068  ramz2  16099  strfvss  16245  ressbasss  16295  ress0  16297  ismred2  16616  acsfn  16672  acsfn0  16673  0ssc  16849  fullfunc  16918  fthfunc  16919  mrelatglb0  17538  cntzssv  18111  symgsssg  18237  efgsfo  18504  dprdsn  18789  lsp0  19368  lss0v  19375  lspsnat  19505  lsppratlem3  19510  lbsexg  19525  resspsrbas  19776  psr1crng  19917  psr1assa  19918  psr1tos  19919  psr1bas2  19920  vr1cl2  19923  ply1lss  19926  ply1subrg  19927  psr1plusg  19952  psr1vsca  19953  psr1mulr  19954  psr1ring  19977  psr1lmod  19979  psr1sca  19980  evpmss  20291  ocv0  20384  ocvz  20385  css1  20397  0opn  21079  toponsspwpw  21097  basdif0  21128  baspartn  21129  0cld  21213  ntr0  21256  cmpfi  21582  refun0  21689  xkouni  21773  xkoccn  21793  alexsubALTlem2  22222  ptcmplem2  22227  tsmsfbas  22301  setsmstopn  22653  restmetu  22745  tngtopn  22824  iccntr  22994  xrge0gsumle  23006  xrge0tsms  23007  metdstri  23024  ovol0  23659  0mbl  23705  itg1le  23879  itgioo  23981  limcnlp  24041  dvbsss  24065  plyssc  24355  fsumharmonic  25151  egrsubgr  26574  0grsubgr  26575  0uhgrsubgr  26576  chocnul  28731  span0  28945  chsup0  28951  ssnnssfz  30085  xrge0tsmsd  30319  ddemeas  30833  dya2iocuni  30879  oms0  30893  0elcarsg  30903  eulerpartlemt  30967  bnj1143  31396  mrsubrn  31945  msubrn  31961  mthmpps  32014  dfpo2  32176  trpredlem1  32254  nulsslt  32436  nulssgt  32437  bj-nuliotaALT  33535  bj-restsn0  33554  bj-restsn10  33555  bj-ismooredr2  33581  mblfinlem2  33984  mblfinlem3  33985  ismblfin  33987  sstotbnd2  34108  isbnd3  34118  ssbnd  34122  heiborlem6  34150  lub0N  35257  glb0N  35261  0psubN  35817  padd01  35879  padd02  35880  pol0N  35977  pcl0N  35990  0psubclN  36011  mzpcompact2lem  38151  itgocn  38570  fvnonrel  38737  clcnvlem  38764  cnvrcl0  38766  cnvtrcl0  38767  0he  38909  ntrclskb  39200  founiiun0  40178  uzfissfz  40332  limcdm0  40638  cncfiooicc  40895  itgvol0  40971  ibliooicc  40974  ovn0  41567  sprssspr  42571  ssnn0ssfz  42967  setrec2fun  43327