Theorem eldifd 3486

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

Hypotheses

Ref	Expression
eldifd.1
eldifd.2

Assertion

Ref	Expression
eldifd

Proof of Theorem eldifd

Step	Hyp	Ref	Expression
1		eldifd.1	. 2
2		eldifd.2	. 2
3		eldif 3485	. 2
4	1, 2, 3	sylanbrc 664	1

Syntax hints:  -.wn 3  ->wi 4  e.wcel 1818  \cdif 3472

This theorem is referenced by:  xpdifid  5440  ressuppssdif  6940  oaf1o  7231  findcard2d  7782  cantnflem1  8129  cantnflem2  8130  cantnflem1OLD  8152  fin23lem26  8726  isf34lem4  8778  isfin7-2  8797  axdc3lem4  8854  axdc4lem  8856  ttukeylem7  8916  pwfseqlem1  9057  pwfseqlem3  9059  hashf1lem1  12504  seqcoll  12512  seqcoll2  12513  rlimcld2  13401  sumrblem  13533  fsumcvg  13534  fsumss  13547  incexclem  13648  prodrblem  13736  fprodcvg  13737  fprodss  13755  ruclem12  13974  prmreclem5  14438  ramub1lem1  14544  mreexd  15039  frgpnabllem1  16877  gsumzaddlem  16934  gsumzaddlemOLD  16936  gsum2d  16999  gsum2dOLD  17000  dmdprdsplitlem  17084  dmdprdsplitlemOLD  17085  pgpfac1lem2  17126  pgpfac1lem3  17128  irredrmul  17356  lsppratlem3  17795  lbsextlem4  17807  psgnodpmr  18626  frlmsslsp  18829  frlmsslspOLD  18830  regsep2  19877  1stckgen  20055  regr1lem  20240  opnsubg  20606  zcld  21318  recld2  21319  bcthlem4  21766  iundisj  21958  iblss2  22212  itgeqa  22220  limcnlp  22282  dvloglem  23029  dvlog2lem  23033  ressatans  23265  wilthlem2  23343  tgelrnln  24010  nbcusgra  24463  usgrasscusgra  24483  uvtxnbgra  24493  frgrancvvdeqlem1  25030  frgrawopreglem4  25047  iundisjf  27448  iundisjfi  27601  elzrhunit  27960  qqhval2  27963  plymulx  28505  signstfvneq0  28529  regamcl  28603  facgam  28608  onint1  29914  dvtanlem  30064  dvasin  30103  areacirclem4  30110  pridlc3  30470  rmspecsqrtnq  30842  rmspecnonsq  30843  icoiccdif  31564  fprodn0f  31594  climrec  31609  limciccioolb  31627  limcrecl  31635  sumnnodd  31636  lptioo2  31637  lptioo1  31638  limcicciooub  31643  lptre2pt  31646  reclimc  31659  icccncfext  31690  fperdvper  31715  dvnmul  31740  itgcoscmulx  31768  itgsincmulx  31773  stoweidlem34  31816  stoweidlem39  31821  stoweidlem57  31839  wallispi  31852  stirlinglem8  31863  dirkercncflem2  31886  dirkercncflem4  31888  fourierdlem38  31927  fourierdlem40  31929  fourierdlem42  31931  fourierdlem46  31935  fourierdlem53  31942  fourierdlem56  31945  fourierdlem58  31947  fourierdlem62  31951  fourierdlem74  31963  fourierdlem75  31964  fourierdlem76  31965  fourierdlem78  31967  fourierdlem93  31982  fourierdlem103  31992  fourierdlem104  31993  fouriersw  32014  elaa2  32017  etransc  32066  usgra2pthlem1  32353

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-v 3111  df-dif 3478