Theorem eldifbd 3553

Description: If a class is in the difference of two classes, it is not in the subtrahend. One-way deduction form of eldif 3550. (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 3550	. . 3 ⊢ (𝐴 ∈ (𝐵 ∖ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶))
3	1, 2	sylib 207	. 2 ⊢ (𝜑 → (𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶))
4	3	simprd 478	1 ⊢ (𝜑 → ¬ 𝐴 ∈ 𝐶)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 383   ∈ wcel 1977   ∖ cdif 3537

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-dif 3543

This theorem is referenced by:  xpdifid  5481  boxcutc  7837  infeq5i  8416  cantnflem2  8470  ackbij1lem18  8942  infpssrlem4  9011  fin23lem30  9047  domtriomlem  9147  pwfseqlem4  9363  dvdsaddre2b  14867  dprdfadd  18242  pgpfac1lem2  18297  pgpfac1lem3a  18298  pgpfac1lem3  18299  lspsolv  18964  lsppratlem3  18970  mplsubrglem  19260  frlmssuvc2  19953  hauscmplem  21019  1stccnp  21075  1stckgen  21167  alexsublem  21658  bcthlem4  22932  plyeq0lem  23770  ftalem3  24601  tglngne  25245  disjiunel  28791  ofpreima2  28849  qqhval2  29354  esum2dlem  29481  carsgclctunlem1  29706  sibfof  29729  sitgaddlemb  29737  eulerpartlemsv2  29747  eulerpartlemv  29753  eulerpartlemgs2  29769  dochnel2  35699  rmspecnonsq  36490  disjiun2  38251  dstregt0  38434  fprodexp  38661  fprodabs2  38662  fprodcnlem  38666  lptre2pt  38707  dvnprodlem2  38837  stoweidlem43  38936  fourierdlem66  39065  hsphoidmvle2  39475  hsphoidmvle  39476  hoidmvlelem1  39485  hoidmvlelem2  39486  hoidmvlelem3  39487  hoidmvlelem4  39488  1loopgrvd0  40719