Theorem eldifbd 3962

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 397   ∈ wcel 2107   ∖ cdif 3946

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-dif 3952

This theorem is referenced by:  xpdifid  6168  boxcutc  8935  infeq5i  9631  cantnflem2  9685  ackbij1lem18  10232  infpssrlem4  10301  fin23lem30  10337  domtriomlem  10437  pwfseqlem4  10657  dvdsaddre2b  16250  dprdfadd  19890  pgpfac1lem2  19945  pgpfac1lem3a  19946  pgpfac1lem3  19947  lspsolv  20756  lsppratlem3  20762  frlmssuvc2  21350  mplsubrglem  21563  hauscmplem  22910  1stccnp  22966  1stckgen  23058  alexsublem  23548  bcthlem4  24844  plyeq0lem  25724  ftalem3  26579  tglngne  27832  1loopgrvd0  28792  disjiunel  31858  ofpreima2  31922  fvdifsupp  31938  nn0difffzod  32047  cycpmco2f1  32314  cycpmco2lem1  32316  cycpmco2lem5  32320  cycpmco2  32323  cyc3co2  32330  tocyccntz  32334  elrspunsn  32578  mxidlmaxv  32615  mxidlirredi  32618  qsdrnglem2  32641  gsummoncoe1fzo  32699  fedgmullem2  32746  qqhval2  32993  esum2dlem  33121  carsgclctunlem1  33347  sibfof  33370  sitgaddlemb  33378  eulerpartlemsv2  33388  eulerpartlemv  33394  eulerpartlemgs2  33410  dochnel2  40311  nelsubginvcld  41118  nelsubgcld  41119  fltne  41434  rmspecnonsq  41693  disjiun2  43793  dstregt0  44039  fprodexp  44358  fprodabs2  44359  fprodcnlem  44363  lptre2pt  44404  dvnprodlem2  44711  stoweidlem43  44807  fourierdlem66  44936  iundjiunlem  45223  hsphoidmvle2  45349  hsphoidmvle  45350  hoidmvlelem1  45359  hoidmvlelem2  45360  hoidmvlelem3  45361  hoidmvlelem4  45362  readdcnnred  46059  resubcnnred  46060  recnmulnred  46061  cndivrenred  46062