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

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

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 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-dif 3902

This theorem is used by:  xpdifid  6162  xpdifcnvepel  6163  fvdifsupp  8174  boxcutc  8955  infeq5i  9622  cantnflem2  9676  ackbij1lem18  10263  infpssrlem4  10333  fin23lem30  10369  domtriomlem  10469  pwfseqlem4  10696  dvdsaddre2b  16422  chnccats1  18738  chnccat  18739  dprdfadd  20175  pgpfac1lem2  20230  pgpfac1lem3a  20231  pgpfac1lem3  20232  lspsolv  21360  lsppratlem3  21366  prmidlsubm  21582  frlmssuvc2  22040  mplsubrglem  22250  hauscmplem  23663  1stccnp  23720  1stckgen  23812  alexsublem  24302  bcthlem4  25587  plyeq0lem  26468  ftalem3  27343  tglngne  28924  oppmir  29143  tgelrnpln  29165  elplng  29169  elplngid  29171  plngcplem  29174  plngrotlem1  29176  plngrotlem2  29177  plngrot  29179  lnssplnglem  29180  lnssplng  29181  plngmiropp  29183  nhpmirhp  29187  prlngex  29340  prlngmolem1  29341  prlngmolem2  29342  prlngmid2  29350  1loopgrvd0  29996  disjiunel  33101  ofpreima2  33171  nn0difffzod  33307  gsumfs2d  33533  suppgsumssiun  33544  cycpmco2f1  33596  cycpmco2lem1  33598  cycpmco2lem5  33602  cycpmco2  33605  cyc3co2  33612  tocyccntz  33616  elrgspnlem2  33715  elrgspnlem4  33717  domnprodeq0  33751  elrspunsn  33890  mxidlmaxv  33904  mxidlirredi  33907  qsdrnglem2  33931  dflringlem  33937  dflringlem2  33938  rprmnz  33963  rprmnunit  33964  rprmirred  33974  rprmdvdsprod  33977  1arithufdlem3  33989  dfufd2  33993  deg1prod  34026  ply1dg3rt0irred  34027  gsummoncoe1fzo  34040  mplidomlem  34070  evlextv  34085  psrgsum  34091  psrmonprod  34095  vieta  34123  fedgmullem2  34173  fldextrspunlsp  34217  extdgfialglem2  34236  qqhval2  34525  esum2dlem  34635  carsgclctunlem1  34861  sibfof  34884  sitgaddlemb  34892  eulerpartlemsv2  34902  eulerpartlemv  34908  eulerpartlemgs2  34924  onvf1od  35787  ttcwf2  37211  dochnel2  42330  evl1gprodd  43048  nelsubginvcld  43449  nelsubgcld  43450  fltne  43555  rmspecnonsq  43813  disjiun2  45957  dstregt0  46180  fprodexp  46489  fprodabs2  46490  fprodcnlem  46494  lptre2pt  46533  dvnprodlem2  46840  stoweidlem43  46936  fourierdlem66  47065  iundjiunlem  47352  hsphoidmvle2  47478  hsphoidmvle  47479  hoidmvlelem1  47488  hoidmvlelem2  47489  hoidmvlelem3  47490  hoidmvlelem4  47491  readdcnnred  48256  resubcnnred  48257  recnmulnred  48258  cndivrenred  48259