Theorem eldifbd 3916

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

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

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 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3438  df-dif 3906

This theorem is referenced by:  xpdifid  6117  fvdifsupp  8104  boxcutc  8868  infeq5i  9532  cantnflem2  9586  ackbij1lem18  10130  infpssrlem4  10200  fin23lem30  10236  domtriomlem  10336  pwfseqlem4  10556  dvdsaddre2b  16218  dprdfadd  19901  pgpfac1lem2  19956  pgpfac1lem3a  19957  pgpfac1lem3  19958  lspsolv  21050  lsppratlem3  21056  frlmssuvc2  21702  mplsubrglem  21911  hauscmplem  23291  1stccnp  23347  1stckgen  23439  alexsublem  23929  bcthlem4  25225  plyeq0lem  26113  ftalem3  26983  tglngne  28495  1loopgrvd0  29450  disjiunel  32540  ofpreima2  32610  nn0difffzod  32750  chnccats1  32958  gsumfs2d  33009  cycpmco2f1  33067  cycpmco2lem1  33069  cycpmco2lem5  33073  cycpmco2  33076  cyc3co2  33083  tocyccntz  33087  elrgspnlem2  33184  elrgspnlem4  33186  elrspunsn  33367  mxidlmaxv  33406  mxidlirredi  33409  qsdrnglem2  33434  rprmnz  33458  rprmnunit  33459  rprmirred  33469  rprmdvdsprod  33472  1arithufdlem3  33484  dfufd2  33488  ply1dg3rt0irred  33519  gsummoncoe1fzo  33531  fedgmullem2  33603  fldextrspunlsp  33647  extdgfialglem2  33666  qqhval2  33955  esum2dlem  34065  carsgclctunlem1  34291  sibfof  34314  sitgaddlemb  34322  eulerpartlemsv2  34332  eulerpartlemv  34338  eulerpartlemgs2  34354  onvf1od  35090  dochnel2  41381  evl1gprodd  42100  nelsubginvcld  42479  nelsubgcld  42480  fltne  42627  rmspecnonsq  42890  disjiun2  45046  dstregt0  45274  fprodexp  45585  fprodabs2  45586  fprodcnlem  45590  lptre2pt  45631  dvnprodlem2  45938  stoweidlem43  46034  fourierdlem66  46163  iundjiunlem  46450  hsphoidmvle2  46576  hsphoidmvle  46577  hoidmvlelem1  46586  hoidmvlelem2  46587  hoidmvlelem3  46588  hoidmvlelem4  46589  readdcnnred  47297  resubcnnred  47298  recnmulnred  47299  cndivrenred  47300