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

Theorem 0ss 4353
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 4299 . . 3 ¬ 𝑥 ∈ ∅
21pm2.21i 119 . 2 (𝑥 ∈ ∅ → 𝑥𝐴)
32ssriv 3974 1 ∅ ⊆ 𝐴
Colors of variables: wff setvar class
Syntax hints:  wcel 2113  wss 3939  c0 4294
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2160  ax-12 2176  ax-ext 2796
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1539  df-ex 1780  df-nf 1784  df-sb 2069  df-clab 2803  df-cleq 2817  df-clel 2896  df-dif 3942  df-in 3946  df-ss 3955  df-nul 4295
This theorem is referenced by:  ss0b  4354  0pss  4399  npss0  4400  ssdifeq0  4435  pwpw0  4749  sssn  4762  sspr  4769  sstp  4770  pwsnOLD  4834  uni0  4869  int0el  4910  0disj  5061  disjx0  5063  tr0  5186  al0ssb  5215  0elpw  5259  rel0  5675  0ima  5949  dmxpss  6031  dmsnopss  6074  on0eqel  6311  iotassuni  6337  fun0  6422  f0  6563  fvmptss  6783  fvmptss2  6796  funressn  6924  riotassuni  7157  frxp  7823  suppssdm  7846  suppun  7853  suppss  7863  suppssov1  7865  suppss2  7867  suppssfv  7869  oaword1  8181  oaword2  8182  omwordri  8201  oewordri  8221  oeworde  8222  nnaword1  8258  0domg  8647  fodomr  8671  pwdom  8672  php  8704  isinf  8734  finsschain  8834  fipwuni  8893  fipwss  8896  wdompwdom  9045  inf3lemd  9093  inf3lem1  9094  cantnfle  9137  tc0  9192  r1val1  9218  alephgeom  9511  infmap2  9643  cfub  9674  cf0  9676  cflecard  9678  cfle  9679  fin23lem16  9760  itunitc1  9845  ttukeylem6  9939  ttukeylem7  9940  canthwe  10076  wun0  10143  tsk0  10188  gruina  10243  grur1a  10244  uzssz  12267  xrsup0  12719  fzoss1  13067  fsuppmapnn0fiubex  13363  swrd00  14009  swrdlend  14018  repswswrd  14149  xptrrel  14343  sum0  15081  fsumss  15085  fsumcvg3  15089  prod0  15300  0bits  15791  sadid1  15820  sadid2  15821  smu01lem  15837  smu01  15838  smu02  15839  lcmf0  15981  vdwmc2  16318  vdwlem13  16332  ramz2  16363  strfvss  16509  ressbasss  16559  ress0  16561  ismred2  16877  acsfn  16933  acsfn0  16934  0ssc  17110  fullfunc  17179  fthfunc  17180  mrelatglb0  17798  cntzssv  18461  symgsssg  18598  efgsfo  18868  dprdsn  19161  lsp0  19784  lss0v  19791  lspsnat  19920  lsppratlem3  19924  lbsexg  19939  resspsrbas  20198  mhp0cl  20340  psr1crng  20358  psr1assa  20359  psr1tos  20360  psr1bas2  20361  vr1cl2  20364  ply1lss  20367  ply1subrg  20368  psr1plusg  20393  psr1vsca  20394  psr1mulr  20395  psr1ring  20418  psr1lmod  20420  psr1sca  20421  evpmss  20733  ocv0  20824  ocvz  20825  css1  20837  0opn  21515  toponsspwpw  21533  basdif0  21564  baspartn  21565  0cld  21649  ntr0  21692  cmpfi  22019  refun0  22126  xkouni  22210  xkoccn  22230  alexsubALTlem2  22659  ptcmplem2  22664  tsmsfbas  22739  setsmstopn  23091  restmetu  23183  tngtopn  23262  iccntr  23432  xrge0gsumle  23444  xrge0tsms  23445  metdstri  23462  ovol0  24097  0mbl  24143  itg1le  24317  itgioo  24419  limcnlp  24479  dvbsss  24503  plyssc  24793  fsumharmonic  25592  egrsubgr  27062  0grsubgr  27063  0uhgrsubgr  27064  chocnul  29108  span0  29322  chsup0  29328  ssnnssfz  30513  xrge0tsmsd  30696  ddemeas  31499  dya2iocuni  31545  oms0  31559  0elcarsg  31569  eulerpartlemt  31633  bnj1143  32066  mrsubrn  32764  msubrn  32780  mthmpps  32833  dfpo2  32995  trpredlem1  33070  nulsslt  33266  nulssgt  33267  bj-nuliotaALT  34355  bj-restsn0  34380  bj-restsn10  34381  pibt2  34702  mblfinlem2  34934  mblfinlem3  34935  ismblfin  34937  sstotbnd2  35056  isbnd3  35066  ssbnd  35070  heiborlem6  35098  lub0N  36329  glb0N  36333  0psubN  36889  padd01  36951  padd02  36952  pol0N  37049  pcl0N  37062  0psubclN  37083  mzpcompact2lem  39354  itgocn  39770  fvnonrel  39963  clcnvlem  39989  cnvrcl0  39991  cnvtrcl0  39992  0he  40134  ntrclskb  40425  gru0eld  40571  mnu0eld  40607  mnuprdlem4  40617  mnuprd  40618  founiiun0  41457  uzfissfz  41600  limcdm0  41905  cncfiooicc  42183  itgvol0  42259  ibliooicc  42262  ovn0  42855  sprssspr  43650  ssnn0ssfz  44404  setrec2fun  44802
  Copyright terms: Public domain W3C validator