Theorem eldifbd 3896

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   ∈ wcel 2108   ∖ cdif 3880

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-dif 3886

This theorem is referenced by:  xpdifid  6060  boxcutc  8687  infeq5i  9324  cantnflem2  9378  ackbij1lem18  9924  infpssrlem4  9993  fin23lem30  10029  domtriomlem  10129  pwfseqlem4  10349  dvdsaddre2b  15944  dprdfadd  19538  pgpfac1lem2  19593  pgpfac1lem3a  19594  pgpfac1lem3  19595  lspsolv  20320  lsppratlem3  20326  frlmssuvc2  20912  mplsubrglem  21120  hauscmplem  22465  1stccnp  22521  1stckgen  22613  alexsublem  23103  bcthlem4  24396  plyeq0lem  25276  ftalem3  26129  tglngne  26815  1loopgrvd0  27774  disjiunel  30836  ofpreima2  30905  fvdifsupp  30920  cycpmco2f1  31293  cycpmco2lem1  31295  cycpmco2lem5  31299  cycpmco2  31302  cyc3co2  31309  tocyccntz  31313  fedgmullem2  31613  qqhval2  31832  esum2dlem  31960  carsgclctunlem1  32184  sibfof  32207  sitgaddlemb  32215  eulerpartlemsv2  32225  eulerpartlemv  32231  eulerpartlemgs2  32247  dochnel2  39333  nelsubginvcld  40146  nelsubgcld  40147  fltne  40397  rmspecnonsq  40645  disjiun2  42495  dstregt0  42709  fprodexp  43025  fprodabs2  43026  fprodcnlem  43030  lptre2pt  43071  dvnprodlem2  43378  stoweidlem43  43474  fourierdlem66  43603  iundjiunlem  43887  hsphoidmvle2  44013  hsphoidmvle  44014  hoidmvlelem1  44023  hoidmvlelem2  44024  hoidmvlelem3  44025  hoidmvlelem4  44026  readdcnnred  44683  resubcnnred  44684  recnmulnred  44685  cndivrenred  44686