Theorem eldifbd 3902

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

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

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-dif 3892

This theorem is referenced by:  xpdifid  6132  fvdifsupp  8121  boxcutc  8889  infeq5i  9557  cantnflem2  9611  ackbij1lem18  10158  infpssrlem4  10228  fin23lem30  10264  domtriomlem  10364  pwfseqlem4  10585  dvdsaddre2b  16276  chnccats1  18591  chnccat  18592  dprdfadd  19997  pgpfac1lem2  20052  pgpfac1lem3a  20053  pgpfac1lem3  20054  lspsolv  21141  lsppratlem3  21147  frlmssuvc2  21775  mplsubrglem  21982  hauscmplem  23371  1stccnp  23427  1stckgen  23519  alexsublem  24009  bcthlem4  25294  plyeq0lem  26175  ftalem3  27038  tglngne  28618  1loopgrvd0  29573  disjiunel  32666  ofpreima2  32739  nn0difffzod  32877  gsumfs2d  33122  suppgsumssiun  33133  cycpmco2f1  33185  cycpmco2lem1  33187  cycpmco2lem5  33191  cycpmco2  33194  cyc3co2  33201  tocyccntz  33205  elrgspnlem2  33304  elrgspnlem4  33306  domnprodeq0  33337  elrspunsn  33489  mxidlmaxv  33528  mxidlirredi  33531  qsdrnglem2  33556  rprmnz  33580  rprmnunit  33581  rprmirred  33591  rprmdvdsprod  33594  1arithufdlem3  33606  dfufd2  33610  deg1prod  33643  ply1dg3rt0irred  33644  gsummoncoe1fzo  33657  evlextv  33686  psrgsum  33692  psrmonprod  33696  vieta  33724  fedgmullem2  33774  fldextrspunlsp  33818  extdgfialglem2  33837  qqhval2  34126  esum2dlem  34236  carsgclctunlem1  34461  sibfof  34484  sitgaddlemb  34492  eulerpartlemsv2  34502  eulerpartlemv  34508  eulerpartlemgs2  34524  onvf1od  35289  ttcwf2  36707  mh-inf3f1  36723  dochnel2  41838  evl1gprodd  42556  nelsubginvcld  42941  nelsubgcld  42942  fltne  43077  rmspecnonsq  43335  disjiun2  45489  dstregt0  45715  fprodexp  46024  fprodabs2  46025  fprodcnlem  46029  lptre2pt  46068  dvnprodlem2  46375  stoweidlem43  46471  fourierdlem66  46600  iundjiunlem  46887  hsphoidmvle2  47013  hsphoidmvle  47014  hoidmvlelem1  47023  hoidmvlelem2  47024  hoidmvlelem3  47025  hoidmvlelem4  47026  chnsubseq  47310  readdcnnred  47751  resubcnnred  47752  recnmulnred  47753  cndivrenred  47754