Theorem sseq0 3975

Description: A subclass of an empty class is empty. (Contributed by NM, 7-Mar-2007.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)

Assertion

Ref	Expression
sseq0	|- ( ( A C_ B /\ B = (/) ) -> A = (/) )

Proof of Theorem sseq0

Step	Hyp	Ref	Expression
1		sseq2 3627	. . 3 |- ( B = (/) -> ( A C_ B <-> A C_ (/) ) )
2		ss0 3974	. . 3 |- ( A C_ (/) -> A = (/) )
3	1, 2	syl6bi 243	. 2 |- ( B = (/) -> ( A C_ B -> A = (/) ) )
4	3	impcom 446	1 |- ( ( A C_ B /\ B = (/) ) -> A = (/) )

Syntax hints:   -> wi 4   /\ wa 384   = wceq 1483   C_ 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:  ssn0  3976  ssdifin0  4050  disjxiun  4649  disjxiunOLD  4650  undom  8048  fieq0  8327  infdifsn  8554  cantnff  8571  tc00  8624  hashun3  13173  strlemor1OLD  15969  strleun  15972  xpsc0  16220  xpsc1  16221  dmdprdsplit2lem  18444  2idlval  19233  opsrle  19475  pf1rcl  19713  ocvval  20011  pjfval  20050  en2top  20789  nrmsep  21161  isnrm3  21163  regsep2  21180  xkohaus  21456  kqdisj  21535  regr1lem  21542  alexsublem  21848  reconnlem1  22629  metdstri  22654  iundisj2  23317  0clwlk0  26992  disjxpin  29401  iundisj2f  29403  iundisj2fi  29556  cvmsss2  31256  cldbnd  32321  cntotbnd  33595  mapfzcons1  37280  onfrALTlem2  38761  onfrALTlem2VD  39125  nnuzdisj  39571