Theorem eldifbd 3805

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-ext 2754

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-v 3400  df-dif 3795

This theorem is referenced by:  xpdifid  5816  boxcutc  8237  infeq5i  8830  cantnflem2  8884  ackbij1lem18  9394  infpssrlem4  9463  fin23lem30  9499  domtriomlem  9599  pwfseqlem4  9819  dvdsaddre2b  15436  dprdfadd  18806  pgpfac1lem2  18861  pgpfac1lem3a  18862  pgpfac1lem3  18863  lspsolv  19539  lsppratlem3  19546  mplsubrglem  19836  frlmssuvc2  20538  hauscmplem  21618  1stccnp  21674  1stckgen  21766  alexsublem  22256  bcthlem4  23533  plyeq0lem  24403  ftalem3  25253  tglngne  25901  1loopgrvd0  26852  disjiunel  29972  ofpreima2  30031  qqhval2  30624  esum2dlem  30752  carsgclctunlem1  30977  sibfof  31000  sitgaddlemb  31008  eulerpartlemsv2  31018  eulerpartlemv  31024  eulerpartlemgs2  31040  dochnel2  37546  nelsubginvcld  38131  nelsubgcld  38132  rmspecnonsq  38431  disjiun2  40157  dstregt0  40403  fprodexp  40734  fprodabs2  40735  fprodcnlem  40739  lptre2pt  40780  dvnprodlem2  41090  stoweidlem43  41187  fourierdlem66  41316  hsphoidmvle2  41726  hsphoidmvle  41727  hoidmvlelem1  41736  hoidmvlelem2  41737  hoidmvlelem3  41738  hoidmvlelem4  41739  readdcnnred  42345  resubcnnred  42346  recnmulnred  42347  cndivrenred  42348