Theorem eldifbd 3927

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

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

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 3449  df-dif 3917

This theorem is referenced by:  xpdifid  6141  fvdifsupp  8150  boxcutc  8914  infeq5i  9589  cantnflem2  9643  ackbij1lem18  10189  infpssrlem4  10259  fin23lem30  10295  domtriomlem  10395  pwfseqlem4  10615  dvdsaddre2b  16277  dprdfadd  19952  pgpfac1lem2  20007  pgpfac1lem3a  20008  pgpfac1lem3  20009  lspsolv  21053  lsppratlem3  21059  frlmssuvc2  21704  mplsubrglem  21913  hauscmplem  23293  1stccnp  23349  1stckgen  23441  alexsublem  23931  bcthlem4  25227  plyeq0lem  26115  ftalem3  26985  tglngne  28477  1loopgrvd0  29432  disjiunel  32525  ofpreima2  32590  nn0difffzod  32729  chnccats1  32941  gsumfs2d  32995  cycpmco2f1  33081  cycpmco2lem1  33083  cycpmco2lem5  33087  cycpmco2  33090  cyc3co2  33097  tocyccntz  33101  elrgspnlem2  33194  elrgspnlem4  33196  elrspunsn  33400  mxidlmaxv  33439  mxidlirredi  33442  qsdrnglem2  33467  rprmnz  33491  rprmnunit  33492  rprmirred  33502  rprmdvdsprod  33505  1arithufdlem3  33517  dfufd2  33521  ply1dg3rt0irred  33551  gsummoncoe1fzo  33563  fedgmullem2  33626  fldextrspunlsp  33669  qqhval2  33972  esum2dlem  34082  carsgclctunlem1  34308  sibfof  34331  sitgaddlemb  34339  eulerpartlemsv2  34349  eulerpartlemv  34355  eulerpartlemgs2  34371  onvf1od  35094  dochnel2  41386  evl1gprodd  42105  nelsubginvcld  42484  nelsubgcld  42485  fltne  42632  rmspecnonsq  42895  disjiun2  45052  dstregt0  45280  fprodexp  45592  fprodabs2  45593  fprodcnlem  45597  lptre2pt  45638  dvnprodlem2  45945  stoweidlem43  46041  fourierdlem66  46170  iundjiunlem  46457  hsphoidmvle2  46583  hsphoidmvle  46584  hoidmvlelem1  46593  hoidmvlelem2  46594  hoidmvlelem3  46595  hoidmvlelem4  46596  readdcnnred  47304  resubcnnred  47305  recnmulnred  47306  cndivrenred  47307