Theorem eldifbd 3898

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 397   ∈ wcel 2121   ∖ cdif 3882

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713

This theorem depends on definitions:  df-bi 209  df-an 398  df-tru 1551  df-ex 1788  df-sb 2075  df-clab 2720  df-cleq 2733  df-clel 2816  df-v 3435  df-dif 3888

This theorem is referenced by:  xpdifid  6123  fvdifsupp  8115  boxcutc  8883  infeq5i  9552  cantnflem2  9606  ackbij1lem18  10153  infpssrlem4  10223  fin23lem30  10259  domtriomlem  10359  pwfseqlem4  10580  dvdsaddre2b  16271  chnccats1  18586  chnccat  18587  dprdfadd  19992  pgpfac1lem2  20047  pgpfac1lem3a  20048  pgpfac1lem3  20049  lspsolv  21140  lsppratlem3  21146  frlmssuvc2  21774  mplsubrglem  21982  hauscmplem  23393  1stccnp  23449  1stckgen  23541  alexsublem  24031  bcthlem4  25316  plyeq0lem  26197  ftalem3  27060  tglngne  28640  1loopgrvd0  29595  disjiunel  32689  ofpreima2  32762  nn0difffzod  32900  gsumfs2d  33146  suppgsumssiun  33157  cycpmco2f1  33209  cycpmco2lem1  33211  cycpmco2lem5  33215  cycpmco2  33218  cyc3co2  33225  tocyccntz  33229  elrgspnlem2  33328  elrgspnlem4  33330  domnprodeq0  33361  elrspunsn  33516  mxidlmaxv  33555  mxidlirredi  33558  qsdrnglem2  33583  dflringlem  33589  dflringlem2  33590  rprmnz  33615  rprmnunit  33616  rprmirred  33626  rprmdvdsprod  33629  1arithufdlem3  33641  dfufd2  33645  deg1prod  33678  ply1dg3rt0irred  33679  gsummoncoe1fzo  33692  mplidomlem  33723  evlextv  33738  psrgsum  33744  psrmonprod  33748  vieta  33776  fedgmullem2  33826  fldextrspunlsp  33870  extdgfialglem2  33889  qqhval2  34178  esum2dlem  34288  carsgclctunlem1  34513  sibfof  34536  sitgaddlemb  34544  eulerpartlemsv2  34554  eulerpartlemv  34560  eulerpartlemgs2  34576  onvf1od  35350  ttcwf2  36768  mh-inf3f1  36784  dochnel2  41899  evl1gprodd  42617  nelsubginvcld  43001  nelsubgcld  43002  fltne  43109  rmspecnonsq  43367  disjiun2  45521  dstregt0  45744  fprodexp  46053  fprodabs2  46054  fprodcnlem  46058  lptre2pt  46097  dvnprodlem2  46404  stoweidlem43  46500  fourierdlem66  46629  iundjiunlem  46916  hsphoidmvle2  47042  hsphoidmvle  47043  hoidmvlelem1  47052  hoidmvlelem2  47053  hoidmvlelem3  47054  hoidmvlelem4  47055  chnsubseq  47339  readdcnnred  47780  resubcnnred  47781  recnmulnred  47782  cndivrenred  47783