Theorem eldifbd 3939

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-v 3461  df-dif 3929

This theorem is referenced by:  xpdifid  6157  fvdifsupp  8170  boxcutc  8955  infeq5i  9650  cantnflem2  9704  ackbij1lem18  10250  infpssrlem4  10320  fin23lem30  10356  domtriomlem  10456  pwfseqlem4  10676  dvdsaddre2b  16326  dprdfadd  20003  pgpfac1lem2  20058  pgpfac1lem3a  20059  pgpfac1lem3  20060  lspsolv  21104  lsppratlem3  21110  frlmssuvc2  21755  mplsubrglem  21964  hauscmplem  23344  1stccnp  23400  1stckgen  23492  alexsublem  23982  bcthlem4  25279  plyeq0lem  26167  ftalem3  27037  tglngne  28529  1loopgrvd0  29484  disjiunel  32577  ofpreima2  32644  nn0difffzod  32783  chnccats1  32995  gsumfs2d  33049  cycpmco2f1  33135  cycpmco2lem1  33137  cycpmco2lem5  33141  cycpmco2  33144  cyc3co2  33151  tocyccntz  33155  elrgspnlem2  33238  elrgspnlem4  33240  elrspunsn  33444  mxidlmaxv  33483  mxidlirredi  33486  qsdrnglem2  33511  rprmnz  33535  rprmnunit  33536  rprmirred  33546  rprmdvdsprod  33549  1arithufdlem3  33561  dfufd2  33565  ply1dg3rt0irred  33595  gsummoncoe1fzo  33607  fedgmullem2  33670  fldextrspunlsp  33715  qqhval2  34013  esum2dlem  34123  carsgclctunlem1  34349  sibfof  34372  sitgaddlemb  34380  eulerpartlemsv2  34390  eulerpartlemv  34396  eulerpartlemgs2  34412  dochnel2  41411  evl1gprodd  42130  nelsubginvcld  42519  nelsubgcld  42520  fltne  42667  rmspecnonsq  42930  disjiun2  45082  dstregt0  45310  fprodexp  45623  fprodabs2  45624  fprodcnlem  45628  lptre2pt  45669  dvnprodlem2  45976  stoweidlem43  46072  fourierdlem66  46201  iundjiunlem  46488  hsphoidmvle2  46614  hsphoidmvle  46615  hoidmvlelem1  46624  hoidmvlelem2  46625  hoidmvlelem3  46626  hoidmvlelem4  46627  readdcnnred  47332  resubcnnred  47333  recnmulnred  47334  cndivrenred  47335