Theorem eldifbd 3488

Description: If a class is in the difference of two classes, it is not in the subtrahend. One-way deduction form of eldif 3485. (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 3485	. . 3
3	1, 2	sylib 196	. 2
4	3	simprd 463	1

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

This theorem is referenced by:  xpdifid  5440  boxcutc  7532  infeq5i  8074  cantnflem2  8130  ackbij1lem18  8638  infpssrlem4  8707  fin23lem30  8743  domtriomlem  8843  pwfseqlem4  9061  dprdfadd  17060  dprdfaddOLD  17067  pgpfac1lem2  17126  pgpfac1lem3a  17127  pgpfac1lem3  17128  lspsolv  17789  lsppratlem3  17795  mplsubrglem  18100  mplsubrglemOLD  18101  frlmssuvc2  18826  frlmssuvc2OLD  18828  hauscmplem  19906  1stccnp  19963  1stckgen  20055  alexsublem  20544  bcthlem4  21766  plyeq0lem  22607  ftalem3  23348  tglngne  23937  ofpreima2  27508  qqhval2  27963  sibfof  28282  eulerpartlemsv2  28297  eulerpartlemv  28303  eulerpartlemgs2  28319  rmspecnonsq  30843  dstregt0  31463  fprodexp  31600  fprodabs2  31602  lptre2pt  31646  dvnprodlem2  31744  stoweidlem43  31825  fourierdlem66  31955  dochnel2  37119

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