Theorem eldifbd 3930

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-v 3452  df-dif 3920

This theorem is referenced by:  xpdifid  6144  fvdifsupp  8153  boxcutc  8917  infeq5i  9596  cantnflem2  9650  ackbij1lem18  10196  infpssrlem4  10266  fin23lem30  10302  domtriomlem  10402  pwfseqlem4  10622  dvdsaddre2b  16284  dprdfadd  19959  pgpfac1lem2  20014  pgpfac1lem3a  20015  pgpfac1lem3  20016  lspsolv  21060  lsppratlem3  21066  frlmssuvc2  21711  mplsubrglem  21920  hauscmplem  23300  1stccnp  23356  1stckgen  23448  alexsublem  23938  bcthlem4  25234  plyeq0lem  26122  ftalem3  26992  tglngne  28484  1loopgrvd0  29439  disjiunel  32532  ofpreima2  32597  nn0difffzod  32736  chnccats1  32948  gsumfs2d  33002  cycpmco2f1  33088  cycpmco2lem1  33090  cycpmco2lem5  33094  cycpmco2  33097  cyc3co2  33104  tocyccntz  33108  elrgspnlem2  33201  elrgspnlem4  33203  elrspunsn  33407  mxidlmaxv  33446  mxidlirredi  33449  qsdrnglem2  33474  rprmnz  33498  rprmnunit  33499  rprmirred  33509  rprmdvdsprod  33512  1arithufdlem3  33524  dfufd2  33528  ply1dg3rt0irred  33558  gsummoncoe1fzo  33570  fedgmullem2  33633  fldextrspunlsp  33676  qqhval2  33979  esum2dlem  34089  carsgclctunlem1  34315  sibfof  34338  sitgaddlemb  34346  eulerpartlemsv2  34356  eulerpartlemv  34362  eulerpartlemgs2  34378  onvf1od  35101  dochnel2  41393  evl1gprodd  42112  nelsubginvcld  42491  nelsubgcld  42492  fltne  42639  rmspecnonsq  42902  disjiun2  45059  dstregt0  45287  fprodexp  45599  fprodabs2  45600  fprodcnlem  45604  lptre2pt  45645  dvnprodlem2  45952  stoweidlem43  46048  fourierdlem66  46177  iundjiunlem  46464  hsphoidmvle2  46590  hsphoidmvle  46591  hoidmvlelem1  46600  hoidmvlelem2  46601  hoidmvlelem3  46602  hoidmvlelem4  46603  readdcnnred  47308  resubcnnred  47309  recnmulnred  47310  cndivrenred  47311