MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  eldifd Unicode version

Theorem eldifd 3299
Description: If a class is in one class and not another, it is also in their difference. One-way deduction form of eldif 3298. (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
StepHypRef Expression
1 eldifd.1 . 2  |-  ( ph  ->  A  e.  B )
2 eldifd.2 . 2  |-  ( ph  ->  -.  A  e.  C
)
3 eldif 3298 . 2  |-  ( A  e.  ( B  \  C )  <->  ( A  e.  B  /\  -.  A  e.  C ) )
41, 2, 3sylanbrc 646 1  |-  ( ph  ->  A  e.  ( B 
\  C ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    e. wcel 1721    \ cdif 3285
This theorem is referenced by:  oaf1o  6773  cantnflem1  7609  cantnflem2  7610  fin23lem26  8169  isf34lem4  8221  isfin7-2  8240  axdc3lem4  8297  axdc4lem  8299  ttukeylem7  8359  pwfseqlem1  8497  pwfseqlem3  8499  hashf1lem1  11667  seqcoll  11675  seqcoll2  11676  rlimcld2  12335  sumrblem  12468  fsumcvg  12469  fsumss  12482  incexclem  12579  ruclem12  12803  prmreclem5  13251  ramub1lem1  13357  mreexd  13830  frgpnabllem1  15447  gsumzaddlem  15489  gsum2d  15509  dmdprdsplitlem  15558  pgpfac1lem2  15596  pgpfac1lem3  15598  irredrmul  15775  lsppratlem3  16184  lbsextlem4  16196  regsep2  17402  1stckgen  17547  regr1lem  17732  opnsubg  18098  zcld  18805  recld2  18806  bcthlem4  19241  iundisj  19403  iblss2  19658  itgeqa  19666  limcnlp  19726  dvloglem  20500  dvlog2lem  20504  ressatans  20735  wilthlem2  20813  nbcusgra  21433  usgrasscusgra  21453  uvtxnbgra  21463  iundisjf  23990  iundisjfi  24113  elzrhunit  24324  qqhval2  24327  regamcl  24806  facgam  24811  prodrblem  25216  fprodcvg  25217  fprodss  25235  onint1  26111  dvreasin  26187  areacirclem5  26193  pridlc3  26581  rmspecsqrnq  26867  rmspecnonsq  26868  frlmsslsp  27124  climrec  27604  stoweidlem34  27658  stoweidlem39  27663  stoweidlem57  27681  wallispi  27694  stirlinglem8  27705  usgra2pthlem1  28048  frgrancvvdeqlem1  28141  frgrawopreglem4  28158
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2393
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2399  df-cleq 2405  df-clel 2408  df-nfc 2537  df-v 2926  df-dif 3291
  Copyright terms: Public domain W3C validator