Theorem eldifbd 3902

Description: If a class is in the difference of two classes, it is not in the subtrahend. One-way deduction form of eldif 3899. (Contributed by David Moews, 1-May-2017.)

Hypothesis

Ref	Expression
eldifbd.1	⊢ (𝜑 → 𝐴 ∈ (𝐵 ∖ 𝐶))

Assertion

Ref	Expression
eldifbd	⊢ (𝜑 → ¬ 𝐴 ∈ 𝐶)

Proof of Theorem eldifbd

Step	Hyp	Ref	Expression
1		eldifbd.1	. . 3 ⊢ (𝜑 → 𝐴 ∈ (𝐵 ∖ 𝐶))
2		eldif 3899	. . 3 ⊢ (𝐴 ∈ (𝐵 ∖ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶))
3	1, 2	sylib 217	. 2 ⊢ (𝜑 → (𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶))
4	3	simprd 495	1 ⊢ (𝜑 → ¬ 𝐴 ∈ 𝐶)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   ∈ wcel 2101   ∖ cdif 3886

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2103  ax-9 2111  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1540  df-ex 1778  df-sb 2063  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3436  df-dif 3892

This theorem is referenced by:  xpdifid  6075  boxcutc  8749  infeq5i  9422  cantnflem2  9476  ackbij1lem18  10021  infpssrlem4  10090  fin23lem30  10126  domtriomlem  10226  pwfseqlem4  10446  dvdsaddre2b  16044  dprdfadd  19651  pgpfac1lem2  19706  pgpfac1lem3a  19707  pgpfac1lem3  19708  lspsolv  20433  lsppratlem3  20439  frlmssuvc2  21030  mplsubrglem  21238  hauscmplem  22585  1stccnp  22641  1stckgen  22733  alexsublem  23223  bcthlem4  24519  plyeq0lem  25399  ftalem3  26252  tglngne  26939  1loopgrvd0  27899  disjiunel  30963  ofpreima2  31031  fvdifsupp  31046  cycpmco2f1  31419  cycpmco2lem1  31421  cycpmco2lem5  31425  cycpmco2  31428  cyc3co2  31435  tocyccntz  31439  fedgmullem2  31739  qqhval2  31960  esum2dlem  32088  carsgclctunlem1  32312  sibfof  32335  sitgaddlemb  32343  eulerpartlemsv2  32353  eulerpartlemv  32359  eulerpartlemgs2  32375  dochnel2  39432  nelsubginvcld  40243  nelsubgcld  40244  fltne  40504  rmspecnonsq  40752  disjiun2  42630  dstregt0  42854  fprodexp  43170  fprodabs2  43171  fprodcnlem  43175  lptre2pt  43216  dvnprodlem2  43523  stoweidlem43  43619  fourierdlem66  43748  iundjiunlem  44033  hsphoidmvle2  44159  hsphoidmvle  44160  hoidmvlelem1  44169  hoidmvlelem2  44170  hoidmvlelem3  44171  hoidmvlelem4  44172  readdcnnred  44835  resubcnnred  44836  recnmulnred  44837  cndivrenred  44838