Theorem eldifbd 3975

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-v 3479  df-dif 3965

This theorem is referenced by:  xpdifid  6189  fvdifsupp  8194  boxcutc  8979  infeq5i  9673  cantnflem2  9727  ackbij1lem18  10273  infpssrlem4  10343  fin23lem30  10379  domtriomlem  10479  pwfseqlem4  10699  dvdsaddre2b  16340  dprdfadd  20054  pgpfac1lem2  20109  pgpfac1lem3a  20110  pgpfac1lem3  20111  lspsolv  21162  lsppratlem3  21168  frlmssuvc2  21832  mplsubrglem  22041  hauscmplem  23429  1stccnp  23485  1stckgen  23577  alexsublem  24067  bcthlem4  25374  plyeq0lem  26263  ftalem3  27132  tglngne  28572  1loopgrvd0  29536  disjiunel  32615  ofpreima2  32682  nn0difffzod  32813  gsumfs2d  33040  cycpmco2f1  33126  cycpmco2lem1  33128  cycpmco2lem5  33132  cycpmco2  33135  cyc3co2  33142  tocyccntz  33146  elrgspnlem2  33232  elrgspnlem4  33234  elrspunsn  33436  mxidlmaxv  33475  mxidlirredi  33478  qsdrnglem2  33503  rprmnz  33527  rprmnunit  33528  rprmirred  33538  rprmdvdsprod  33541  1arithufdlem3  33553  dfufd2  33557  ply1dg3rt0irred  33586  gsummoncoe1fzo  33597  fedgmullem2  33657  qqhval2  33944  esum2dlem  34072  carsgclctunlem1  34298  sibfof  34321  sitgaddlemb  34329  eulerpartlemsv2  34339  eulerpartlemv  34345  eulerpartlemgs2  34361  dochnel2  41374  evl1gprodd  42098  nelsubginvcld  42482  nelsubgcld  42483  fltne  42630  rmspecnonsq  42894  disjiun2  44997  dstregt0  45231  fprodexp  45549  fprodabs2  45550  fprodcnlem  45554  lptre2pt  45595  dvnprodlem2  45902  stoweidlem43  45998  fourierdlem66  46127  iundjiunlem  46414  hsphoidmvle2  46540  hsphoidmvle  46541  hoidmvlelem1  46550  hoidmvlelem2  46551  hoidmvlelem3  46552  hoidmvlelem4  46553  readdcnnred  47252  resubcnnred  47253  recnmulnred  47254  cndivrenred  47255