MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  0ss Structured version   Visualization version   GIF version

Theorem 0ss 3950
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.
StepHypRef Expression
1 noel 3901 . . 3 ¬ 𝑥 ∈ ∅
21pm2.21i 116 . 2 (𝑥 ∈ ∅ → 𝑥𝐴)
32ssriv 3592 1 ∅ ⊆ 𝐴
Colors of variables: wff setvar class
Syntax hints:  wcel 1987  wss 3560  c0 3897
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-v 3192  df-dif 3563  df-in 3567  df-ss 3574  df-nul 3898
This theorem is referenced by:  ss0b  3951  0pss  3991  npss0  3992  npss0OLD  3993  ssdifeq0  4029  pwpw0  4319  sssn  4333  sspr  4341  sstp  4342  pwsnALT  4404  uni0  4438  int0el  4480  0disj  4615  disjx0  4617  tr0  4734  0elpw  4804  rel0  5214  0ima  5451  dmxpss  5534  dmsnopss  5576  on0eqel  5814  iotassuni  5836  fun0  5922  fresaunres2  6043  f0  6053  fvmptss  6259  fvmptss2  6270  funressn  6391  riotassuni  6613  frxp  7247  suppssdm  7268  suppun  7275  suppss  7285  suppssov1  7287  suppss2  7289  suppssfv  7291  oaword1  7592  oaword2  7593  omwordri  7612  oewordri  7632  oeworde  7633  nnaword1  7669  0domg  8047  fodomr  8071  pwdom  8072  php  8104  isinf  8133  finsschain  8233  fipwuni  8292  fipwss  8295  wdompwdom  8443  inf3lemd  8484  inf3lem1  8485  cantnfle  8528  tc0  8583  r1val1  8609  alephgeom  8865  infmap2  9000  cfub  9031  cf0  9033  cflecard  9035  cfle  9036  fin23lem16  9117  itunitc1  9202  ttukeylem6  9296  ttukeylem7  9297  canthwe  9433  wun0  9500  tsk0  9545  gruina  9600  grur1a  9601  uzssz  11667  xrsup0  12112  fzoss1  12452  fsuppmapnn0fiubex  12748  swrd00  13372  swrdlend  13385  swrd0  13388  repswswrd  13484  xptrrel  13669  sum0  14401  fsumss  14405  fsumcvg3  14409  prod0  14617  0bits  15104  sadid1  15133  sadid2  15134  smu01lem  15150  smu01  15151  smu02  15152  lcmf0  15290  vdwmc2  15626  vdwlem13  15640  ramz2  15671  strfvss  15821  ressbasss  15872  ress0  15874  strlemor0OLD  15908  ismred2  16203  acsfn  16260  acsfn0  16261  0ssc  16437  fullfunc  16506  fthfunc  16507  mrelatglb0  17125  cntzssv  17701  symgsssg  17827  efgsfo  18092  dprdsn  18375  lsp0  18949  lss0v  18956  lspsnat  19085  lsppratlem3  19089  lbsexg  19104  resspsrbas  19355  psr1crng  19497  psr1assa  19498  psr1tos  19499  psr1bas2  19500  vr1cl2  19503  ply1lss  19506  ply1subrg  19507  psr1plusg  19532  psr1vsca  19533  psr1mulr  19534  psr1ring  19557  psr1lmod  19559  psr1sca  19560  evpmss  19872  ocv0  19961  ocvz  19962  css1  19974  0opn  20649  toponsspwpw  20666  basdif0  20697  baspartn  20698  0cld  20782  cls0  20824  ntr0  20825  cmpfi  21151  refun0  21258  xkouni  21342  xkoccn  21362  alexsubALTlem2  21792  ptcmplem2  21797  tsmsfbas  21871  setsmstopn  22223  restmetu  22315  tngtopn  22394  iccntr  22564  xrge0gsumle  22576  xrge0tsms  22577  metdstri  22594  ovol0  23201  0mbl  23247  itg1le  23420  itgioo  23522  limcnlp  23582  dvbsss  23606  plyssc  23894  fsumharmonic  24672  egrsubgr  26096  0grsubgr  26097  0uhgrsubgr  26098  chocnul  28075  span0  28289  chsup0  28295  ssnnssfz  29432  xrge0tsmsd  29612  ddemeas  30122  dya2iocuni  30168  oms0  30182  0elcarsg  30192  eulerpartlemt  30256  bnj1143  30622  mrsubrn  31171  msubrn  31187  mthmpps  31240  dfpo2  31406  trpredlem1  31481  bj-nuliotaALT  32720  bj-restsn0  32728  bj-restsn10  32729  mblfinlem2  33118  mblfinlem3  33119  ismblfin  33121  sstotbnd2  33244  isbnd3  33254  ssbnd  33258  heiborlem6  33286  lub0N  33995  glb0N  33999  0psubN  34554  padd01  34616  padd02  34617  pol0N  34714  pcl0N  34727  0psubclN  34748  mzpcompact2lem  36833  itgocn  37254  fvnonrel  37423  clcnvlem  37450  cnvrcl0  37452  cnvtrcl0  37453  0he  37597  ntrclskb  37888  founiiun0  38886  uzfissfz  39041  limcdm0  39286  cncfiooicc  39442  itgvol0  39521  ibliooicc  39524  ovn0  40117  sprssspr  41049  ssnn0ssfz  41445  setrec2fun  41762
  Copyright terms: Public domain W3C validator