Theorem ssneldd 3606

Description: If an element is not in a class, it is also not in a subclass of that class. Deduction form. (Contributed by David Moews, 1-May-2017.)

Hypotheses

Ref	Expression
ssneld.1	|- ( ph -> A C_ B )
ssneldd.2	|- ( ph -> -. C e. B )

Assertion

Ref	Expression
ssneldd	|- ( ph -> -. C e. A )

Proof of Theorem ssneldd

Step	Hyp	Ref	Expression
1		ssneldd.2	. 2 |- ( ph -> -. C e. B )
2		ssneld.1	. . 3 |- ( ph -> A C_ B )
3	2	ssneld 3605	. 2 |- ( ph -> ( -. C e. B -> -. C e. A ) )
4	1, 3	mpd 15	1 |- ( ph -> -. C e. A )

Syntax hints:   -. wn 3   -> wi 4   e. wcel 1990   C_ wss 3574

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-in 3581  df-ss 3588

This theorem is referenced by:  0nelrel  5162  cantnfp1lem3  8577  fpwwe2lem13  9464  pwfseqlem3  9482  hashbclem  13236  sumrblem  14442  incexclem  14568  prodrblem  14659  fprodntriv  14672  ramub1lem2  15731  mreexmrid  16303  mreexexlem2d  16305  acsfiindd  17177  lbspss  19082  lbsextlem4  19161  lindfrn  20160  fclscmpi  21833  lhop2  23778  lhop  23779  dvcnvrelem1  23780  axlowdimlem17  25838  erdszelem8  31180  osumcllem10N  35251  pexmidlem7N  35262  mapdindp2  37010  mapdindp3  37011  hdmapval3lemN  37129  hdmap11lem1  37133  fourierdlem80  40403