Theorem eldifbd 3949

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-v 3496  df-dif 3939

This theorem is referenced by:  xpdifid  6025  boxcutc  8505  infeq5i  9099  cantnflem2  9153  ackbij1lem18  9659  infpssrlem4  9728  fin23lem30  9764  domtriomlem  9864  pwfseqlem4  10084  dvdsaddre2b  15657  dprdfadd  19142  pgpfac1lem2  19197  pgpfac1lem3a  19198  pgpfac1lem3  19199  lspsolv  19915  lsppratlem3  19921  mplsubrglem  20219  frlmssuvc2  20939  hauscmplem  22014  1stccnp  22070  1stckgen  22162  alexsublem  22652  bcthlem4  23930  plyeq0lem  24800  ftalem3  25652  tglngne  26336  1loopgrvd0  27286  disjiunel  30346  ofpreima2  30411  fvdifsupp  30427  cycpmco2f1  30766  cycpmco2lem1  30768  cycpmco2lem5  30772  cycpmco2  30775  cyc3co2  30782  tocyccntz  30786  fedgmullem2  31026  qqhval2  31223  esum2dlem  31351  carsgclctunlem1  31575  sibfof  31598  sitgaddlemb  31606  eulerpartlemsv2  31616  eulerpartlemv  31622  eulerpartlemgs2  31638  dochnel2  38543  nelsubginvcld  39148  nelsubgcld  39149  fltne  39292  rmspecnonsq  39524  disjiun2  41340  dstregt0  41567  fprodexp  41895  fprodabs2  41896  fprodcnlem  41900  lptre2pt  41941  dvnprodlem2  42252  stoweidlem43  42348  fourierdlem66  42477  hsphoidmvle2  42887  hsphoidmvle  42888  hoidmvlelem1  42897  hoidmvlelem2  42898  hoidmvlelem3  42899  hoidmvlelem4  42900  readdcnnred  43523  resubcnnred  43524  recnmulnred  43525  cndivrenred  43526