Theorem eldifbd 3919

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 399   ∈ wcel 2144   ∖ cdif 3903

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-ext 2736

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1565  df-ex 1802  df-sb 2093  df-clab 2743  df-cleq 2756  df-clel 2839  df-v 3458  df-dif 3909

This theorem is referenced by:  xpdifid  6155  xpdifcnvepel  6156  fvdifsupp  8153  boxcutc  8925  infeq5i  9593  cantnflem2  9647  ackbij1lem18  10194  infpssrlem4  10265  fin23lem30  10301  domtriomlem  10401  pwfseqlem4  10622  dvdsaddre2b  16343  chnccats1  18659  chnccat  18660  dprdfadd  20064  pgpfac1lem2  20119  pgpfac1lem3a  20120  pgpfac1lem3  20121  lspsolv  21215  lsppratlem3  21221  frlmssuvc2  21849  mplsubrglem  22057  hauscmplem  23468  1stccnp  23524  1stckgen  23616  alexsublem  24106  bcthlem4  25391  plyeq0lem  26272  ftalem3  27141  tglngne  28721  tgelrnpln  28985  elplng  28989  elplngid  28991  plngcplem  28994  plngrotlem1  28996  plngrotlem2  28997  plngrot  28999  lnssplnglem  29000  lnssplng  29001  1loopgrvd0  29707  disjiunel  32798  ofpreima2  32870  nn0difffzod  33008  gsumfs2d  33243  suppgsumssiun  33254  cycpmco2f1  33306  cycpmco2lem1  33308  cycpmco2lem5  33312  cycpmco2  33315  cyc3co2  33322  tocyccntz  33326  elrgspnlem2  33426  elrgspnlem4  33428  domnprodeq0  33462  elrspunsn  33617  prmidlsubm  33648  mxidlmaxv  33658  mxidlirredi  33661  qsdrnglem2  33686  dflringlem  33692  dflringlem2  33693  rprmnz  33718  rprmnunit  33719  rprmirred  33729  rprmdvdsprod  33732  1arithufdlem3  33744  dfufd2  33748  deg1prod  33781  ply1dg3rt0irred  33782  gsummoncoe1fzo  33795  mplidomlem  33826  evlextv  33841  psrgsum  33847  psrmonprod  33851  vieta  33879  fedgmullem2  33929  fldextrspunlsp  33973  extdgfialglem2  33992  qqhval2  34281  esum2dlem  34391  carsgclctunlem1  34616  sibfof  34639  sitgaddlemb  34647  eulerpartlemsv2  34657  eulerpartlemv  34663  eulerpartlemgs2  34679  onvf1od  35454  ttcwf2  36890  mh-inf3f1  36906  dochnel2  42021  evl1gprodd  42739  nelsubginvcld  43123  nelsubgcld  43124  fltne  43231  rmspecnonsq  43489  disjiun2  45643  dstregt0  45866  fprodexp  46175  fprodabs2  46176  fprodcnlem  46180  lptre2pt  46219  dvnprodlem2  46526  stoweidlem43  46622  fourierdlem66  46751  iundjiunlem  47038  hsphoidmvle2  47164  hsphoidmvle  47165  hoidmvlelem1  47174  hoidmvlelem2  47175  hoidmvlelem3  47176  hoidmvlelem4  47177  chnsubseq  47461  readdcnnred  47902  resubcnnred  47903  recnmulnred  47904  cndivrenred  47905