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

Theorem eldifad 3292
Description: If a class is in the difference of two classes, it is also in the minuend. One-way deduction form of eldif 3290. (Contributed by David Moews, 1-May-2017.)
Hypothesis
Ref Expression
eldifad.1  |-  ( ph  ->  A  e.  ( B 
\  C ) )
Assertion
Ref Expression
eldifad  |-  ( ph  ->  A  e.  B )

Proof of Theorem eldifad
StepHypRef Expression
1 eldifad.1 . . 3  |-  ( ph  ->  A  e.  ( B 
\  C ) )
2 eldif 3290 . . 3  |-  ( A  e.  ( B  \  C )  <->  ( A  e.  B  /\  -.  A  e.  C ) )
31, 2sylib 189 . 2  |-  ( ph  ->  ( A  e.  B  /\  -.  A  e.  C
) )
43simpld 446 1  |-  ( ph  ->  A  e.  B )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 359    e. wcel 1721    \ cdif 3277
This theorem is referenced by:  unblem1  7318  cantnflem3  7603  cantnflem4  7604  oef1o  7611  infxpenc  7855  acndom2  7891  ackbij1lem18  8073  infpssrlem3  8141  fin23lem26  8161  fin23lem30  8178  pwfseqlem4a  8492  expclz  11361  efgsdmi  15319  efgs1b  15323  efgsp1  15324  efgsres  15325  efgredlemf  15328  efgredlemd  15331  efgredlem  15334  efgrelexlemb  15337  gsum2d2lem  15502  pgpfac1lem2  15588  pgpfac1lem3a  15589  pgpfac1lem3  15590  pgpfac1lem4  15591  isdrng2  15800  lvecinv  16140  lspsncmp  16143  lspsnne1  16144  lspsnnecom  16146  lspabs2  16147  lspsneu  16150  lspdisjb  16153  lspexch  16156  lspindp1  16160  lvecindp2  16166  lspsolv  16170  lspsnat  16172  lsppratlem1  16174  lsppratlem2  16175  fidomndrnglem  16321  hauscmplem  17423  1stccnp  17478  imasdsf1olem  18356  dvrec  19794  ftc1lem6  19878  elqaalem1  20189  elqaalem3  20191  ulmdvlem3  20271  abelthlem6  20305  abelthlem7a  20306  abelthlem7  20307  logtayl  20504  ftalem3  20810  lgsqrlem1  21078  lgsqrlem2  21079  lgsqrlem3  21080  lgsqrlem4  21081  lgseisenlem1  21086  lgseisenlem2  21087  lgseisenlem3  21088  lgseisenlem4  21089  lgseisen  21090  lgsquadlem2  21092  lgsquadlem3  21093  chebbnd1lem1  21116  dchrisum0re  21160  dchrisum0lema  21161  dchrisum0lem1b  21162  dchrisum0lem1  21163  dchrisum0lem2a  21164  dchrisum0lem2  21165  uhgrass  21294  umgraex  21311  qqhval2  24319  esummono  24403  gsumesum  24404  measvuni  24521  sitgclg  24609  dmgmn0  24763  dmgmaddnn0  24764  dmgmdivn0  24765  lgamgulmlem2  24767  lgamgulmlem3  24768  lgamgulmlem5  24770  lgamgulmlem6  24771  lgamgulm2  24773  lgambdd  24774  lgamucov  24775  lgamcvg2  24792  gamcvg  24793  gamcvg2lem  24796  iprodgam  25272  rrndstprj2  26430  qirropth  26861  rmxyneg  26873  rmxm1  26887  rmxluc  26889  rmxdbl  26892  ltrmxnn0  26904  jm2.19lem1  26950  jm2.23  26957  rmxdiophlem  26976  aomclem2  27020  frlmssuvc2  27115  pmtrfinv  27270  symggen  27279  climrec  27596  climdivf  27605  stoweidlem34  27650  stoweidlem43  27659  lsatelbN  29489  lsatfixedN  29492  lkreqN  29653  lkrlspeqN  29654  dochnel2  31875  dochnel  31876  djhcvat42  31898  dochsnshp  31936  dochexmidat  31942  dochsnkr  31955  dochsnkr2  31956  dochsnkr2cl  31957  dochflcl  31958  dochfl1  31959  dochfln0  31960  lcfl6lem  31981  lcfl7lem  31982  lcfl8b  31987  lclkrlem2a  31990  lclkrlem2b  31991  lclkrlem2c  31992  lclkrlem2d  31993  lclkrlem2e  31994  lclkrlem2f  31995  lcfrlem14  32039  lcfrlem15  32040  lcfrlem16  32041  lcfrlem17  32042  lcfrlem18  32043  lcfrlem19  32044  lcfrlem20  32045  lcfrlem21  32046  lcfrlem23  32048  lcfrlem25  32050  lcfrlem26  32051  lcfrlem35  32060  lcfrlem36  32061  mapdn0  32152  mapdpglem29  32183  mapdpglem24  32187  baerlem3lem1  32190  baerlem5alem1  32191  baerlem5blem1  32192  baerlem3lem2  32193  baerlem5alem2  32194  baerlem5blem2  32195  baerlem5amN  32199  baerlem5bmN  32200  baerlem5abmN  32201  mapdindp0  32202  mapdindp1  32203  mapdindp2  32204  mapdindp3  32205  mapdindp4  32206  mapdheq2  32212  mapdheq4lem  32214  mapdheq4  32215  mapdh6lem1N  32216  mapdh6lem2N  32217  mapdh6aN  32218  mapdh6bN  32220  mapdh6cN  32221  mapdh6dN  32222  mapdh6eN  32223  mapdh6fN  32224  mapdh6gN  32225  mapdh6hN  32226  mapdh6iN  32227  mapdh7eN  32231  mapdh7cN  32232  mapdh7dN  32233  mapdh7fN  32234  mapdh75e  32235  mapdh75fN  32238  hvmaplfl  32250  mapdhvmap  32252  mapdh8aa  32259  mapdh8ab  32260  mapdh8ad  32262  mapdh8b  32263  mapdh8c  32264  mapdh8d0N  32265  mapdh8d  32266  mapdh8e  32267  mapdh9a  32273  hdmap1val2  32284  hdmap1eq  32285  hdmap1valc  32287  hdmap1eq2  32289  hdmap1eq4N  32290  hdmap1l6lem1  32291  hdmap1l6lem2  32292  hdmap1l6a  32293  hdmap1l6b  32295  hdmap1l6c  32296  hdmap1l6d  32297  hdmap1l6e  32298  hdmap1l6f  32299  hdmap1l6g  32300  hdmap1l6h  32301  hdmap1l6i  32302  hdmap1eulem  32307  hdmap1neglem1N  32311  hdmapcl  32316  hdmapval2lem  32317  hdmapval0  32319  hdmapeveclem  32320  hdmapevec  32321  hdmapval3lemN  32323  hdmapval3N  32324  hdmap10lem  32325  hdmap11lem1  32327  hdmap11lem2  32328  hdmapnzcl  32331  hdmaprnlem3N  32336  hdmaprnlem3uN  32337  hdmaprnlem4N  32339  hdmaprnlem7N  32341  hdmaprnlem8N  32342  hdmaprnlem9N  32343  hdmaprnlem3eN  32344  hdmaprnlem16N  32348  hdmap14lem1  32354  hdmap14lem2N  32355  hdmap14lem3  32356  hdmap14lem4a  32357  hdmap14lem6  32359  hdmap14lem8  32361  hdmap14lem9  32362  hdmap14lem10  32363  hdmap14lem11  32364  hdmap14lem12  32365  hgmaprnlem1N  32382  hgmaprnlem2N  32383  hgmaprnlem3N  32384  hgmaprnlem4N  32385  hdmapip1  32402  hdmapinvlem1  32404  hdmapinvlem2  32405  hdmapinvlem3  32406  hdmapinvlem4  32407  hdmapglem5  32408  hgmapvvlem1  32409  hgmapvvlem2  32410  hgmapvvlem3  32411  hdmapglem7a  32413  hdmapglem7b  32414  hdmapglem7  32415
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 2385
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 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-v 2918  df-dif 3283
  Copyright terms: Public domain W3C validator