Theorem 0ss 3972

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

Syntax hints:   ∈ wcel 1990   ⊆ wss 3574  ∅c0 3915

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-dif 3577  df-in 3581  df-ss 3588  df-nul 3916

This theorem is referenced by:  ss0b  3973  0pss  4013  npss0  4014  npss0OLD  4015  ssdifeq0  4051  pwpw0  4344  sssn  4358  sspr  4366  sstp  4367  pwsnALT  4429  uni0  4465  int0el  4508  0disj  4645  disjx0  4647  tr0  4764  0elpw  4834  rel0  5243  0ima  5482  dmxpss  5565  dmsnopss  5607  on0eqel  5845  iotassuni  5867  fun0  5954  fresaunres2  6076  f0  6086  fvmptss  6292  fvmptss2  6304  funressn  6426  riotassuni  6648  frxp  7287  suppssdm  7308  suppun  7315  suppss  7325  suppssov1  7327  suppss2  7329  suppssfv  7331  oaword1  7632  oaword2  7633  omwordri  7652  oewordri  7672  oeworde  7673  nnaword1  7709  0domg  8087  fodomr  8111  pwdom  8112  php  8144  isinf  8173  finsschain  8273  fipwuni  8332  fipwss  8335  wdompwdom  8483  inf3lemd  8524  inf3lem1  8525  cantnfle  8568  tc0  8623  r1val1  8649  alephgeom  8905  infmap2  9040  cfub  9071  cf0  9073  cflecard  9075  cfle  9076  fin23lem16  9157  itunitc1  9242  ttukeylem6  9336  ttukeylem7  9337  canthwe  9473  wun0  9540  tsk0  9585  gruina  9640  grur1a  9641  uzssz  11707  xrsup0  12153  fzoss1  12495  fsuppmapnn0fiubex  12792  swrd00  13418  swrdlend  13431  swrd0  13434  repswswrd  13531  xptrrel  13719  sum0  14452  fsumss  14456  fsumcvg3  14460  prod0  14673  0bits  15161  sadid1  15190  sadid2  15191  smu01lem  15207  smu01  15208  smu02  15209  lcmf0  15347  vdwmc2  15683  vdwlem13  15697  ramz2  15728  strfvss  15880  ressbasss  15932  ress0  15934  strlemor0OLD  15968  ismred2  16263  acsfn  16320  acsfn0  16321  0ssc  16497  fullfunc  16566  fthfunc  16567  mrelatglb0  17185  cntzssv  17761  symgsssg  17887  efgsfo  18152  dprdsn  18435  lsp0  19009  lss0v  19016  lspsnat  19145  lsppratlem3  19149  lbsexg  19164  resspsrbas  19415  psr1crng  19557  psr1assa  19558  psr1tos  19559  psr1bas2  19560  vr1cl2  19563  ply1lss  19566  ply1subrg  19567  psr1plusg  19592  psr1vsca  19593  psr1mulr  19594  psr1ring  19617  psr1lmod  19619  psr1sca  19620  evpmss  19932  ocv0  20021  ocvz  20022  css1  20034  0opn  20709  toponsspwpw  20726  basdif0  20757  baspartn  20758  0cld  20842  cls0  20884  ntr0  20885  cmpfi  21211  refun0  21318  xkouni  21402  xkoccn  21422  alexsubALTlem2  21852  ptcmplem2  21857  tsmsfbas  21931  setsmstopn  22283  restmetu  22375  tngtopn  22454  iccntr  22624  xrge0gsumle  22636  xrge0tsms  22637  metdstri  22654  ovol0  23261  0mbl  23307  itg1le  23480  itgioo  23582  limcnlp  23642  dvbsss  23666  plyssc  23956  fsumharmonic  24738  egrsubgr  26169  0grsubgr  26170  0uhgrsubgr  26171  chocnul  28187  span0  28401  chsup0  28407  ssnnssfz  29549  xrge0tsmsd  29785  ddemeas  30299  dya2iocuni  30345  oms0  30359  0elcarsg  30369  eulerpartlemt  30433  bnj1143  30861  mrsubrn  31410  msubrn  31426  mthmpps  31479  dfpo2  31645  trpredlem1  31727  nulsslt  31908  nulssgt  31909  bj-nuliotaALT  33020  bj-restsn0  33038  bj-restsn10  33039  bj-ismooredr2  33065  mblfinlem2  33447  mblfinlem3  33448  ismblfin  33450  sstotbnd2  33573  isbnd3  33583  ssbnd  33587  heiborlem6  33615  lub0N  34476  glb0N  34480  0psubN  35035  padd01  35097  padd02  35098  pol0N  35195  pcl0N  35208  0psubclN  35229  mzpcompact2lem  37314  itgocn  37734  fvnonrel  37903  clcnvlem  37930  cnvrcl0  37932  cnvtrcl0  37933  0he  38076  ntrclskb  38367  founiiun0  39377  uzfissfz  39542  limcdm0  39850  cncfiooicc  40107  itgvol0  40184  ibliooicc  40187  ovn0  40780  sprssspr  41731  ssnn0ssfz  42127  setrec2fun  42439