Theorem eldifd 3585

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

Syntax hints:   -. wn 3   -> wi 4   e. 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:  eqoreldif  4225  eqoreldifOLD  4226  xpdifid  5562  ressuppssdif  7316  oaf1o  7643  findcard2d  8202  cantnflem1  8586  cantnflem2  8587  fin23lem26  9147  isf34lem4  9199  isfin7-2  9218  axdc3lem4  9275  axdc4lem  9277  ttukeylem7  9337  pwfseqlem1  9480  pwfseqlem3  9482  hashf1lem1  13239  seqcoll  13248  seqcoll2  13249  rlimcld2  14309  sumrblem  14442  fsumcvg  14443  fsumss  14456  incexclem  14568  prodrblem  14659  fprodcvg  14660  fprodss  14678  fprodn0f  14722  ruclem12  14970  coprmproddvdslem  15376  nnoddn2prmb  15518  prmreclem5  15624  ramub1lem1  15730  mreexd  16302  frgpnabllem1  18276  gsumzaddlem  18321  gsum2d  18371  dmdprdsplitlem  18436  pgpfac1lem2  18474  pgpfac1lem3  18476  irredrmul  18707  lsppratlem3  19149  lbsextlem4  19161  psgnodpmr  19936  frlmsslsp  20135  regsep2  21180  1stckgen  21357  regr1lem  21542  opnsubg  21911  zcld  22616  recld2  22617  bcthlem4  23124  iundisj  23316  iblss2  23572  itgeqa  23580  limcnlp  23642  dvloglem  24394  dvlog2lem  24398  ressatans  24661  regamcl  24787  facgam  24792  wilthlem2  24795  2lgslem2  25120  tgelrnln  25525  incistruhgr  25974  upgrres1  26205  usgr2pthlem  26659  iundisjf  29402  iundisjfi  29555  submateqlem1  29873  submateqlem2  29874  elzrhunit  30023  qqhval2  30026  esumrnmpt2  30130  inelpisys  30217  plymulx  30625  signstfvneq0  30649  noetalem3  31865  onint1  32448  lindsenlbs  33404  poimirlem23  33432  poimirlem30  33439  dvasin  33496  areacirclem4  33503  pridlc3  33872  rmspecsqrtnq  37470  rmspecsqrtnqOLD  37471  rmspecnonsq  37472  disjf1o  39378  difmap  39399  difmapsn  39404  supminfxr2  39699  icoiccdif  39750  iccdificc  39766  climrec  39835  limciccioolb  39853  limcrecl  39861  sumnnodd  39862  lptioo2  39863  lptioo1  39864  limcicciooub  39869  lptre2pt  39872  reclimc  39885  cnrefiisplem  40055  icccncfext  40100  fperdvper  40133  dvnmul  40158  itgcoscmulx  40185  itgsincmulx  40190  stoweidlem34  40251  stoweidlem39  40256  stoweidlem57  40274  wallispi  40287  stirlinglem8  40298  dirkercncflem2  40321  dirkercncflem4  40323  fourierdlem38  40362  fourierdlem40  40364  fourierdlem42  40366  fourierdlem46  40369  fourierdlem53  40376  fourierdlem56  40379  fourierdlem58  40381  fourierdlem62  40385  fourierdlem74  40397  fourierdlem75  40398  fourierdlem76  40399  fourierdlem78  40401  fourierdlem93  40416  fourierdlem103  40426  fourierdlem104  40427  fouriersw  40448  elaa2  40451  etransc  40500  gsumge0cl  40588  sge0fodjrnlem  40633  iundjiun  40677  meadjiunlem  40682  meaiininclem  40700  caragendifcl  40728  caratheodorylem1  40740  hoidmvlelem1  40809  hoidmvlelem2  40810  hoidmvlelem4  40812  hspdifhsp  40830  hspmbllem2  40841  preimagelt  40912  preimalegt  40913  dig1  42402