Theorem eldifbd 3924

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

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

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3446  df-dif 3914

This theorem is referenced by:  xpdifid  6129  fvdifsupp  8127  boxcutc  8891  infeq5i  9565  cantnflem2  9619  ackbij1lem18  10165  infpssrlem4  10235  fin23lem30  10271  domtriomlem  10371  pwfseqlem4  10591  dvdsaddre2b  16253  dprdfadd  19936  pgpfac1lem2  19991  pgpfac1lem3a  19992  pgpfac1lem3  19993  lspsolv  21085  lsppratlem3  21091  frlmssuvc2  21737  mplsubrglem  21946  hauscmplem  23326  1stccnp  23382  1stckgen  23474  alexsublem  23964  bcthlem4  25260  plyeq0lem  26148  ftalem3  27018  tglngne  28530  1loopgrvd0  29485  disjiunel  32575  ofpreima2  32640  nn0difffzod  32779  chnccats1  32987  gsumfs2d  33038  cycpmco2f1  33096  cycpmco2lem1  33098  cycpmco2lem5  33102  cycpmco2  33105  cyc3co2  33112  tocyccntz  33116  elrgspnlem2  33210  elrgspnlem4  33212  elrspunsn  33393  mxidlmaxv  33432  mxidlirredi  33435  qsdrnglem2  33460  rprmnz  33484  rprmnunit  33485  rprmirred  33495  rprmdvdsprod  33498  1arithufdlem3  33510  dfufd2  33514  ply1dg3rt0irred  33544  gsummoncoe1fzo  33556  fedgmullem2  33619  fldextrspunlsp  33662  qqhval2  33965  esum2dlem  34075  carsgclctunlem1  34301  sibfof  34324  sitgaddlemb  34332  eulerpartlemsv2  34342  eulerpartlemv  34348  eulerpartlemgs2  34364  onvf1od  35087  dochnel2  41379  evl1gprodd  42098  nelsubginvcld  42477  nelsubgcld  42478  fltne  42625  rmspecnonsq  42888  disjiun2  45045  dstregt0  45273  fprodexp  45585  fprodabs2  45586  fprodcnlem  45590  lptre2pt  45631  dvnprodlem2  45938  stoweidlem43  46034  fourierdlem66  46163  iundjiunlem  46450  hsphoidmvle2  46576  hsphoidmvle  46577  hoidmvlelem1  46586  hoidmvlelem2  46587  hoidmvlelem3  46588  hoidmvlelem4  46589  readdcnnred  47297  resubcnnred  47298  recnmulnred  47299  cndivrenred  47300