Theorem eldifd 3327

Description: If a class is in one class and not another, it is also in their difference. One-way deduction form of eldif 3326. (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 3326	. 2 |- ( A e. ( B \ C ) <-> ( A e. B /\ -. A e. C ) )
4	1, 2, 3	sylanbrc 657	1 |- ( ph -> A e. ( B \ C ) )

Syntax hints:   -. wn 3   -> wi 4   e. wcel 1755   \ cdif 3313

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-v 2964  df-dif 3319

This theorem is referenced by:  xpdifid  5254  ressuppssdif  6699  oaf1o  6990  findcard2d  7542  cantnflem1  7885  cantnflem2  7886  cantnflem1OLD  7908  fin23lem26  8482  isf34lem4  8534  isfin7-2  8553  axdc3lem4  8610  axdc4lem  8612  ttukeylem7  8672  pwfseqlem1  8812  pwfseqlem3  8814  hashf1lem1  12191  seqcoll  12199  seqcoll2  12200  rlimcld2  13039  sumrblem  13171  fsumcvg  13172  fsumss  13185  incexclem  13281  ruclem12  13505  prmreclem5  13963  ramub1lem1  14069  mreexd  14562  frgpnabllem1  16330  gsumzaddlem  16387  gsumzaddlemOLD  16389  gsum2d  16436  gsum2dOLD  16437  dmdprdsplitlem  16507  dmdprdsplitlemOLD  16508  pgpfac1lem2  16549  pgpfac1lem3  16551  irredrmul  16732  lsppratlem3  17151  lbsextlem4  17163  psgnodpmr  17861  frlmsslsp  18064  frlmsslspOLD  18065  regsep2  18821  1stckgen  18968  regr1lem  19153  opnsubg  19519  zcld  20231  recld2  20232  bcthlem4  20679  iundisj  20870  iblss2  21124  itgeqa  21132  limcnlp  21194  dvloglem  21977  dvlog2lem  21981  ressatans  22213  wilthlem2  22291  tgelrnln  22906  tghilbert1_1  22913  nbcusgra  23193  usgrasscusgra  23213  uvtxnbgra  23223  iundisjf  25754  iundisjfi  25902  elzrhunit  26261  qqhval2  26264  plymulx  26796  signstfvneq0  26820  regamcl  26894  facgam  26899  prodrblem  27288  fprodcvg  27289  fprodss  27307  onint1  28142  dvtanlem  28282  dvasin  28321  areacirclem4  28328  pridlc3  28714  rmspecsqrnq  29089  rmspecnonsq  29090  climrec  29619  stoweidlem34  29672  stoweidlem39  29677  stoweidlem57  29695  wallispi  29708  stirlinglem8  29719  usgra2pthlem1  30143  frgrancvvdeqlem1  30466  frgrawopreglem4  30483