Theorem eldifbd 4055

Description: If a class is in the difference of two classes, it is not in the subtrahend. One-way deduction form of eldif 4052. (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 4052	. . 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 2147   ∖ cdif 4048

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-dif 4050

This theorem is used by:  xpdifid  6170  xpdifcnvepel  6171  fvdifsupp  8213  boxcutc  8994  infeq5i  9661  cantnflem2  9715  ackbij1lem18  10338  infpssrlem4  10408  fin23lem30  10444  domtriomlem  10544  pwfseqlem4  10771  dvdsaddre2b  16503  chnccats1  18825  chnccat  18826  dprdfadd  20263  pgpfac1lem2  20318  pgpfac1lem3a  20319  pgpfac1lem3  20320  lspsolv  21448  lsppratlem3  21454  prmidlsubm  21670  frlmssuvc2  22128  mplsubrglem  22338  hauscmplem  23751  1stccnp  23808  1stckgen  23900  alexsublem  24390  bcthlem4  25675  plyeq0lem  26556  ftalem3  27429  fltne  28002  tglngne  29040  oppmir  29259  tgelrnpln  29281  elplng  29285  elplngid  29287  plngcplem  29290  plngrotlem1  29292  plngrotlem2  29293  plngrot  29295  lnssplnglem  29296  lnssplng  29297  plngmiropp  29299  nhpmirhp  29303  prlngex  29456  prlngmolem1  29457  prlngmolem2  29458  prlngmid2  29466  1loopgrvd0  30112  disjiunel  33259  ofpreima2  33329  nn0difffzod  33463  gsumfs2d  33689  suppgsumssiun  33700  cycpmco2f1  33752  cycpmco2lem1  33754  cycpmco2lem5  33758  cycpmco2  33761  cyc3co2  33768  tocyccntz  33772  elrgspnlem2  33871  elrgspnlem4  33873  domnprodeq0  33907  elrspunsn  34046  mxidlmaxv  34060  mxidlirredi  34063  qsdrnglem2  34087  dflringlem  34093  dflringlem2  34094  rprmnz  34119  rprmnunit  34120  rprmirred  34130  rprmdvdsprod  34133  1arithufdlem3  34145  dfufd2  34149  deg1prod  34182  ply1dg3rt0irred  34183  gsummoncoe1fzo  34196  mplidomlem  34226  evlextv  34241  psrgsum  34247  psrmonprod  34251  vieta  34279  fedgmullem2  34329  fldextrspunlsp  34373  extdgfialglem2  34392  qqhval2  34681  esum2dlem  34791  carsgclctunlem1  35016  sibfof  35039  sitgaddlemb  35047  eulerpartlemsv2  35057  eulerpartlemv  35063  eulerpartlemgs2  35079  onvf1od  36034  ttcwf2  37490  dochnel2  42640  evl1gprodd  43358  nelsubginvcld  43751  nelsubgcld  43752  rmspecnonsq  44105  disjiun2  46278  dstregt0  46501  fprodexp  46809  fprodabs2  46810  fprodcnlem  46814  lptre2pt  46853  dvnprodlem2  47160  stoweidlem43  47256  fourierdlem66  47385  iundjiunlem  47672  hsphoidmvle2  47798  hsphoidmvle  47799  hoidmvlelem1  47808  hoidmvlelem2  47809  hoidmvlelem3  47810  hoidmvlelem4  47811  readdcnnred  48576  resubcnnred  48577  recnmulnred  48578  cndivrenred  48579