Theorem eldifbd 3912

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-v 3440  df-dif 3902

This theorem is referenced by:  xpdifid  6124  fvdifsupp  8111  boxcutc  8877  infeq5i  9543  cantnflem2  9597  ackbij1lem18  10144  infpssrlem4  10214  fin23lem30  10250  domtriomlem  10350  pwfseqlem4  10571  dvdsaddre2b  16232  chnccats1  18546  chnccat  18547  dprdfadd  19949  pgpfac1lem2  20004  pgpfac1lem3a  20005  pgpfac1lem3  20006  lspsolv  21096  lsppratlem3  21102  frlmssuvc2  21748  mplsubrglem  21957  hauscmplem  23348  1stccnp  23404  1stckgen  23496  alexsublem  23986  bcthlem4  25281  plyeq0lem  26169  ftalem3  27039  tglngne  28571  1loopgrvd0  29527  disjiunel  32620  ofpreima2  32693  nn0difffzod  32833  gsumfs2d  33093  cycpmco2f1  33155  cycpmco2lem1  33157  cycpmco2lem5  33161  cycpmco2  33164  cyc3co2  33171  tocyccntz  33175  elrgspnlem2  33274  elrgspnlem4  33276  domnprodeq0  33307  elrspunsn  33459  mxidlmaxv  33498  mxidlirredi  33501  qsdrnglem2  33526  rprmnz  33550  rprmnunit  33551  rprmirred  33561  rprmdvdsprod  33564  1arithufdlem3  33576  dfufd2  33580  deg1prod  33613  ply1dg3rt0irred  33614  gsummoncoe1fzo  33627  evlextv  33656  vieta  33685  fedgmullem2  33736  fldextrspunlsp  33780  extdgfialglem2  33799  qqhval2  34088  esum2dlem  34198  carsgclctunlem1  34423  sibfof  34446  sitgaddlemb  34454  eulerpartlemsv2  34464  eulerpartlemv  34470  eulerpartlemgs2  34486  onvf1od  35250  dochnel2  41591  evl1gprodd  42310  nelsubginvcld  42693  nelsubgcld  42694  fltne  42829  rmspecnonsq  43091  disjiun2  45245  dstregt0  45472  fprodexp  45782  fprodabs2  45783  fprodcnlem  45787  lptre2pt  45826  dvnprodlem2  46133  stoweidlem43  46229  fourierdlem66  46358  iundjiunlem  46645  hsphoidmvle2  46771  hsphoidmvle  46772  hoidmvlelem1  46781  hoidmvlelem2  46782  hoidmvlelem3  46783  hoidmvlelem4  46784  chnsubseq  47066  readdcnnred  47491  resubcnnred  47492  recnmulnred  47493  cndivrenred  47494