Theorem eldifbd 3866

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 399   ∈ wcel 2112   ∖ cdif 3850

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1546  df-ex 1788  df-sb 2073  df-clab 2715  df-cleq 2728  df-clel 2809  df-v 3400  df-dif 3856

This theorem is referenced by:  xpdifid  6011  boxcutc  8600  infeq5i  9229  cantnflem2  9283  ackbij1lem18  9816  infpssrlem4  9885  fin23lem30  9921  domtriomlem  10021  pwfseqlem4  10241  dvdsaddre2b  15831  dprdfadd  19361  pgpfac1lem2  19416  pgpfac1lem3a  19417  pgpfac1lem3  19418  lspsolv  20134  lsppratlem3  20140  frlmssuvc2  20711  mplsubrglem  20920  hauscmplem  22257  1stccnp  22313  1stckgen  22405  alexsublem  22895  bcthlem4  24178  plyeq0lem  25058  ftalem3  25911  tglngne  26595  1loopgrvd0  27546  disjiunel  30608  ofpreima2  30677  fvdifsupp  30692  cycpmco2f1  31064  cycpmco2lem1  31066  cycpmco2lem5  31070  cycpmco2  31073  cyc3co2  31080  tocyccntz  31084  fedgmullem2  31379  qqhval2  31598  esum2dlem  31726  carsgclctunlem1  31950  sibfof  31973  sitgaddlemb  31981  eulerpartlemsv2  31991  eulerpartlemv  31997  eulerpartlemgs2  32013  dochnel2  39092  nelsubginvcld  39874  nelsubgcld  39875  fltne  40125  rmspecnonsq  40373  disjiun2  42220  dstregt0  42433  fprodexp  42753  fprodabs2  42754  fprodcnlem  42758  lptre2pt  42799  dvnprodlem2  43106  stoweidlem43  43202  fourierdlem66  43331  iundjiunlem  43615  hsphoidmvle2  43741  hsphoidmvle  43742  hoidmvlelem1  43751  hoidmvlelem2  43752  hoidmvlelem3  43753  hoidmvlelem4  43754  readdcnnred  44411  resubcnnred  44412  recnmulnred  44413  cndivrenred  44414