Theorem eldifd 3344

Description: If a class is in one class and not another, it is also in their difference. One-way deduction form of eldif 3343. (Contributed by David Moews, 1-May-2017.)

Hypotheses

Ref	Expression
eldifd.1	|- ( ph -> A e. B )
eldifd.2	|- ( ph -> -. A e. C )

Assertion

Ref	Expression
eldifd	|- ( ph -> A e. ( B \ C ) )

Proof of Theorem eldifd

Step	Hyp	Ref	Expression
1		eldifd.1	. 2 |- ( ph -> A e. B )
2		eldifd.2	. 2 |- ( ph -> -. A e. C )
3		eldif 3343	. 2 |- ( A e. ( B \ C ) <-> ( A e. B /\ -. A e. C ) )
4	1, 2, 3	sylanbrc 664	1 |- ( ph -> A e. ( B \ C ) )

Syntax hints:   -. wn 3   -> wi 4   e. wcel 1756   \ cdif 3330

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2573  df-v 2979  df-dif 3336

This theorem is referenced by:  xpdifid  5271  ressuppssdif  6715  oaf1o  7007  findcard2d  7559  cantnflem1  7902  cantnflem2  7903  cantnflem1OLD  7925  fin23lem26  8499  isf34lem4  8551  isfin7-2  8570  axdc3lem4  8627  axdc4lem  8629  ttukeylem7  8689  pwfseqlem1  8830  pwfseqlem3  8832  hashf1lem1  12213  seqcoll  12221  seqcoll2  12222  rlimcld2  13061  sumrblem  13193  fsumcvg  13194  fsumss  13207  incexclem  13304  ruclem12  13528  prmreclem5  13986  ramub1lem1  14092  mreexd  14585  frgpnabllem1  16356  gsumzaddlem  16413  gsumzaddlemOLD  16415  gsum2d  16468  gsum2dOLD  16469  dmdprdsplitlem  16539  dmdprdsplitlemOLD  16540  pgpfac1lem2  16581  pgpfac1lem3  16583  irredrmul  16804  lsppratlem3  17235  lbsextlem4  17247  psgnodpmr  18025  frlmsslsp  18228  frlmsslspOLD  18229  regsep2  18985  1stckgen  19132  regr1lem  19317  opnsubg  19683  zcld  20395  recld2  20396  bcthlem4  20843  iundisj  21034  iblss2  21288  itgeqa  21296  limcnlp  21358  dvloglem  22098  dvlog2lem  22102  ressatans  22334  wilthlem2  22412  tgelrnln  23041  tghilbert1_1  23048  nbcusgra  23376  usgrasscusgra  23396  uvtxnbgra  23406  iundisjf  25936  iundisjfi  26085  elzrhunit  26413  qqhval2  26416  plymulx  26954  signstfvneq0  26978  regamcl  27052  facgam  27057  prodrblem  27447  fprodcvg  27448  fprodss  27466  onint1  28300  dvtanlem  28446  dvasin  28485  areacirclem4  28492  pridlc3  28878  rmspecsqrnq  29252  rmspecnonsq  29253  climrec  29781  stoweidlem34  29834  stoweidlem39  29839  stoweidlem57  29857  wallispi  29870  stirlinglem8  29881  usgra2pthlem1  30305  frgrancvvdeqlem1  30628  frgrawopreglem4  30645