Theorem eldifbd 3587

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 384   ∈ wcel 1990   ∖ cdif 3571

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-dif 3577

This theorem is referenced by:  xpdifid  5562  boxcutc  7951  infeq5i  8533  cantnflem2  8587  ackbij1lem18  9059  infpssrlem4  9128  fin23lem30  9164  domtriomlem  9264  pwfseqlem4  9484  dvdsaddre2b  15029  dprdfadd  18419  pgpfac1lem2  18474  pgpfac1lem3a  18475  pgpfac1lem3  18476  lspsolv  19143  lsppratlem3  19149  mplsubrglem  19439  frlmssuvc2  20134  hauscmplem  21209  1stccnp  21265  1stckgen  21357  alexsublem  21848  bcthlem4  23124  plyeq0lem  23966  ftalem3  24801  tglngne  25445  1loopgrvd0  26400  disjiunel  29409  ofpreima2  29466  qqhval2  30026  esum2dlem  30154  carsgclctunlem1  30379  sibfof  30402  sitgaddlemb  30410  eulerpartlemsv2  30420  eulerpartlemv  30426  eulerpartlemgs2  30442  dochnel2  36681  rmspecnonsq  37472  disjiun2  39226  dstregt0  39493  fprodexp  39826  fprodabs2  39827  fprodcnlem  39831  lptre2pt  39872  dvnprodlem2  40162  stoweidlem43  40260  fourierdlem66  40389  hsphoidmvle2  40799  hsphoidmvle  40800  hoidmvlelem1  40809  hoidmvlelem2  40810  hoidmvlelem3  40811  hoidmvlelem4  40812