Theorem eldifbd 3960

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 394   ∈ wcel 2099   ∖ cdif 3944

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2697

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2704  df-cleq 2718  df-clel 2803  df-v 3464  df-dif 3950

This theorem is referenced by:  xpdifid  6179  fvdifsupp  8185  boxcutc  8970  infeq5i  9679  cantnflem2  9733  ackbij1lem18  10280  infpssrlem4  10349  fin23lem30  10385  domtriomlem  10485  pwfseqlem4  10705  dvdsaddre2b  16309  dprdfadd  20020  pgpfac1lem2  20075  pgpfac1lem3a  20076  pgpfac1lem3  20077  lspsolv  21124  lsppratlem3  21130  frlmssuvc2  21793  mplsubrglem  22013  hauscmplem  23401  1stccnp  23457  1stckgen  23549  alexsublem  24039  bcthlem4  25346  plyeq0lem  26237  ftalem3  27103  tglngne  28477  1loopgrvd0  29441  disjiunel  32516  ofpreima2  32583  nn0difffzod  32708  cycpmco2f1  33002  cycpmco2lem1  33004  cycpmco2lem5  33008  cycpmco2  33011  cyc3co2  33018  tocyccntz  33022  elrspunsn  33304  mxidlmaxv  33343  mxidlirredi  33346  qsdrnglem2  33371  rprmnz  33395  rprmnunit  33396  rprmirred  33406  rprmdvdsprod  33409  1arithufdlem3  33421  dfufd2  33425  ply1dg3rt0irred  33454  gsummoncoe1fzo  33465  fedgmullem2  33525  qqhval2  33797  esum2dlem  33925  carsgclctunlem1  34151  sibfof  34174  sitgaddlemb  34182  eulerpartlemsv2  34192  eulerpartlemv  34198  eulerpartlemgs2  34214  dochnel2  41091  evl1gprodd  41815  nelsubginvcld  41975  nelsubgcld  41976  fltne  42298  rmspecnonsq  42564  disjiun2  44659  dstregt0  44896  fprodexp  45215  fprodabs2  45216  fprodcnlem  45220  lptre2pt  45261  dvnprodlem2  45568  stoweidlem43  45664  fourierdlem66  45793  iundjiunlem  46080  hsphoidmvle2  46206  hsphoidmvle  46207  hoidmvlelem1  46216  hoidmvlelem2  46217  hoidmvlelem3  46218  hoidmvlelem4  46219  readdcnnred  46916  resubcnnred  46917  recnmulnred  46918  cndivrenred  46919