Theorem eldifbd 3915

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∧ wa 401   ∈ wcel 2145   ∖ cdif 3899

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3455  df-dif 3905

This theorem is used by:  xpdifid  6164  xpdifcnvepel  6165  fvdifsupp  8172  boxcutc  8951  infeq5i  9618  cantnflem2  9672  ackbij1lem18  10241  infpssrlem4  10311  fin23lem30  10347  domtriomlem  10447  pwfseqlem4  10672  dvdsaddre2b  16399  chnccats1  18715  chnccat  18716  dprdfadd  20148  pgpfac1lem2  20203  pgpfac1lem3a  20204  pgpfac1lem3  20205  lspsolv  21329  lsppratlem3  21335  prmidlsubm  21549  frlmssuvc2  22007  mplsubrglem  22217  hauscmplem  23630  1stccnp  23687  1stckgen  23779  alexsublem  24269  bcthlem4  25554  plyeq0lem  26435  ftalem3  27307  tglngne  28888  oppmir  29107  tgelrnpln  29129  elplng  29133  elplngid  29135  plngcplem  29138  plngrotlem1  29140  plngrotlem2  29141  plngrot  29143  lnssplnglem  29144  lnssplng  29145  plngmiropp  29147  nhpmirhp  29151  prlngex  29292  prlngmolem1  29293  prlngmolem2  29294  prlngmid2  29302  1loopgrvd0  29948  disjiunel  33054  ofpreima2  33124  nn0difffzod  33260  gsumfs2d  33486  suppgsumssiun  33497  cycpmco2f1  33549  cycpmco2lem1  33551  cycpmco2lem5  33555  cycpmco2  33558  cyc3co2  33565  tocyccntz  33569  elrgspnlem2  33668  elrgspnlem4  33670  domnprodeq0  33704  elrspunsn  33842  mxidlmaxv  33856  mxidlirredi  33859  qsdrnglem2  33883  dflringlem  33889  dflringlem2  33890  rprmnz  33915  rprmnunit  33916  rprmirred  33926  rprmdvdsprod  33929  1arithufdlem3  33941  dfufd2  33945  deg1prod  33978  ply1dg3rt0irred  33979  gsummoncoe1fzo  33992  mplidomlem  34022  evlextv  34037  psrgsum  34043  psrmonprod  34047  vieta  34075  fedgmullem2  34125  fldextrspunlsp  34169  extdgfialglem2  34188  qqhval2  34477  esum2dlem  34587  carsgclctunlem1  34813  sibfof  34836  sitgaddlemb  34844  eulerpartlemsv2  34854  eulerpartlemv  34860  eulerpartlemgs2  34876  onvf1od  35689  ttcwf2  37129  mh-inf3f1  37145  dochnel2  42250  evl1gprodd  42968  nelsubginvcld  43369  nelsubgcld  43370  fltne  43475  rmspecnonsq  43733  disjiun2  45877  dstregt0  46100  fprodexp  46409  fprodabs2  46410  fprodcnlem  46414  lptre2pt  46453  dvnprodlem2  46760  stoweidlem43  46856  fourierdlem66  46985  iundjiunlem  47272  hsphoidmvle2  47398  hsphoidmvle  47399  hoidmvlelem1  47408  hoidmvlelem2  47409  hoidmvlelem3  47410  hoidmvlelem4  47411  readdcnnred  48176  resubcnnred  48177  recnmulnred  48178  cndivrenred  48179