Theorem eldifbd 3989

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-dif 3979

This theorem is referenced by:  xpdifid  6199  fvdifsupp  8212  boxcutc  8999  infeq5i  9705  cantnflem2  9759  ackbij1lem18  10305  infpssrlem4  10375  fin23lem30  10411  domtriomlem  10511  pwfseqlem4  10731  dvdsaddre2b  16355  dprdfadd  20064  pgpfac1lem2  20119  pgpfac1lem3a  20120  pgpfac1lem3  20121  lspsolv  21168  lsppratlem3  21174  frlmssuvc2  21838  mplsubrglem  22047  hauscmplem  23435  1stccnp  23491  1stckgen  23583  alexsublem  24073  bcthlem4  25380  plyeq0lem  26269  ftalem3  27136  tglngne  28576  1loopgrvd0  29540  disjiunel  32618  ofpreima2  32684  nn0difffzod  32811  cycpmco2f1  33117  cycpmco2lem1  33119  cycpmco2lem5  33123  cycpmco2  33126  cyc3co2  33133  tocyccntz  33137  elrspunsn  33422  mxidlmaxv  33461  mxidlirredi  33464  qsdrnglem2  33489  rprmnz  33513  rprmnunit  33514  rprmirred  33524  rprmdvdsprod  33527  1arithufdlem3  33539  dfufd2  33543  ply1dg3rt0irred  33572  gsummoncoe1fzo  33583  fedgmullem2  33643  qqhval2  33928  esum2dlem  34056  carsgclctunlem1  34282  sibfof  34305  sitgaddlemb  34313  eulerpartlemsv2  34323  eulerpartlemv  34329  eulerpartlemgs2  34345  dochnel2  41349  evl1gprodd  42074  nelsubginvcld  42451  nelsubgcld  42452  fltne  42599  rmspecnonsq  42863  disjiun2  44960  dstregt0  45196  fprodexp  45515  fprodabs2  45516  fprodcnlem  45520  lptre2pt  45561  dvnprodlem2  45868  stoweidlem43  45964  fourierdlem66  46093  iundjiunlem  46380  hsphoidmvle2  46506  hsphoidmvle  46507  hoidmvlelem1  46516  hoidmvlelem2  46517  hoidmvlelem3  46518  hoidmvlelem4  46519  readdcnnred  47218  resubcnnred  47219  recnmulnred  47220  cndivrenred  47221