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

Theorem eldifd 3333
Description: If a class is in one class and not another, it is also in their difference. One-way deduction form of eldif 3332. (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 3332 . 2  |-  ( A  e.  ( B  \  C )  <->  ( A  e.  B  /\  -.  A  e.  C ) )
41, 2, 3sylanbrc 647 1  |-  ( ph  ->  A  e.  ( B 
\  C ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    e. wcel 1726    \ cdif 3319
This theorem is referenced by:  oaf1o  6809  cantnflem1  7648  cantnflem2  7649  fin23lem26  8210  isf34lem4  8262  isfin7-2  8281  axdc3lem4  8338  axdc4lem  8340  ttukeylem7  8400  pwfseqlem1  8538  pwfseqlem3  8540  hashf1lem1  11709  seqcoll  11717  seqcoll2  11718  rlimcld2  12377  sumrblem  12510  fsumcvg  12511  fsumss  12524  incexclem  12621  ruclem12  12845  prmreclem5  13293  ramub1lem1  13399  mreexd  13872  frgpnabllem1  15489  gsumzaddlem  15531  gsum2d  15551  dmdprdsplitlem  15600  pgpfac1lem2  15638  pgpfac1lem3  15640  irredrmul  15817  lsppratlem3  16226  lbsextlem4  16238  regsep2  17445  1stckgen  17591  regr1lem  17776  opnsubg  18142  zcld  18849  recld2  18850  bcthlem4  19285  iundisj  19447  iblss2  19700  itgeqa  19708  limcnlp  19770  dvloglem  20544  dvlog2lem  20548  ressatans  20779  wilthlem2  20857  nbcusgra  21477  usgrasscusgra  21497  uvtxnbgra  21507  iundisjf  24034  iundisjfi  24157  elzrhunit  24368  qqhval2  24371  regamcl  24850  facgam  24855  prodrblem  25260  fprodcvg  25261  fprodss  25279  onint1  26204  dvtanlem  26268  dvreasin  26304  areacirclem4  26309  pridlc3  26697  rmspecsqrnq  26983  rmspecnonsq  26984  frlmsslsp  27239  climrec  27719  stoweidlem34  27773  stoweidlem39  27778  stoweidlem57  27796  wallispi  27809  stirlinglem8  27820  usgra2pthlem1  28348  frgrancvvdeqlem1  28493  frgrawopreglem4  28510
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-v 2960  df-dif 3325
  Copyright terms: Public domain W3C validator