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 218	. 2 ⊢ (𝜑 → (𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶))
4	3	simprd 495	1 ⊢ (𝜑 → ¬ 𝐴 ∈ 𝐶)

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3443  df-dif 3905

This theorem is referenced by:  xpdifid  6127  fvdifsupp  8115  boxcutc  8883  infeq5i  9549  cantnflem2  9603  ackbij1lem18  10150  infpssrlem4  10220  fin23lem30  10256  domtriomlem  10356  pwfseqlem4  10577  dvdsaddre2b  16238  chnccats1  18552  chnccat  18553  dprdfadd  19955  pgpfac1lem2  20010  pgpfac1lem3a  20011  pgpfac1lem3  20012  lspsolv  21102  lsppratlem3  21108  frlmssuvc2  21754  mplsubrglem  21963  hauscmplem  23354  1stccnp  23410  1stckgen  23502  alexsublem  23992  bcthlem4  25287  plyeq0lem  26175  ftalem3  27045  tglngne  28626  1loopgrvd0  29582  disjiunel  32674  ofpreima2  32747  nn0difffzod  32886  gsumfs2d  33146  cycpmco2f1  33208  cycpmco2lem1  33210  cycpmco2lem5  33214  cycpmco2  33217  cyc3co2  33224  tocyccntz  33228  elrgspnlem2  33327  elrgspnlem4  33329  domnprodeq0  33360  elrspunsn  33512  mxidlmaxv  33551  mxidlirredi  33554  qsdrnglem2  33579  rprmnz  33603  rprmnunit  33604  rprmirred  33614  rprmdvdsprod  33617  1arithufdlem3  33629  dfufd2  33633  deg1prod  33666  ply1dg3rt0irred  33667  gsummoncoe1fzo  33680  evlextv  33709  vieta  33738  fedgmullem2  33789  fldextrspunlsp  33833  extdgfialglem2  33852  qqhval2  34141  esum2dlem  34251  carsgclctunlem1  34476  sibfof  34499  sitgaddlemb  34507  eulerpartlemsv2  34517  eulerpartlemv  34523  eulerpartlemgs2  34539  onvf1od  35303  dochnel2  41720  evl1gprodd  42439  nelsubginvcld  42818  nelsubgcld  42819  fltne  42954  rmspecnonsq  43216  disjiun2  45370  dstregt0  45597  fprodexp  45907  fprodabs2  45908  fprodcnlem  45912  lptre2pt  45951  dvnprodlem2  46258  stoweidlem43  46354  fourierdlem66  46483  iundjiunlem  46770  hsphoidmvle2  46896  hsphoidmvle  46897  hoidmvlelem1  46906  hoidmvlelem2  46907  hoidmvlelem3  46908  hoidmvlelem4  46909  chnsubseq  47191  readdcnnred  47616  resubcnnred  47617  recnmulnred  47618  cndivrenred  47619