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

Theorem eldifad 3324
Description: If a class is in the difference of two classes, it is also in the minuend. One-way deduction form of eldif 3322. (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 3322 . . 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 1725    \ cdif 3309
This theorem is referenced by:  unblem1  7351  cantnflem3  7639  cantnflem4  7640  oef1o  7647  infxpenc  7891  acndom2  7927  ackbij1lem18  8109  infpssrlem3  8177  fin23lem26  8197  fin23lem30  8214  pwfseqlem4a  8528  expclz  11398  efgsdmi  15356  efgs1b  15360  efgsp1  15361  efgsres  15362  efgredlemf  15365  efgredlemd  15368  efgredlem  15371  efgrelexlemb  15374  gsum2d2lem  15539  pgpfac1lem2  15625  pgpfac1lem3a  15626  pgpfac1lem3  15627  pgpfac1lem4  15628  isdrng2  15837  lvecinv  16177  lspsncmp  16180  lspsnne1  16181  lspsnnecom  16183  lspabs2  16184  lspsneu  16187  lspdisjb  16190  lspexch  16193  lspindp1  16197  lvecindp2  16203  lspsolv  16207  lspsnat  16209  lsppratlem1  16211  lsppratlem2  16212  fidomndrnglem  16358  hauscmplem  17461  1stccnp  17517  imasdsf1olem  18395  dvrec  19833  ftc1lem6  19917  elqaalem1  20228  elqaalem3  20230  ulmdvlem3  20310  abelthlem6  20344  abelthlem7a  20345  abelthlem7  20346  logtayl  20543  ftalem3  20849  lgsqrlem1  21117  lgsqrlem2  21118  lgsqrlem3  21119  lgsqrlem4  21120  lgseisenlem1  21125  lgseisenlem2  21126  lgseisenlem3  21127  lgseisenlem4  21128  lgseisen  21129  lgsquadlem2  21131  lgsquadlem3  21132  chebbnd1lem1  21155  dchrisum0re  21199  dchrisum0lema  21200  dchrisum0lem1b  21201  dchrisum0lem1  21202  dchrisum0lem2a  21203  dchrisum0lem2  21204  uhgrass  21333  umgraex  21350  qqhval2  24358  esummono  24442  gsumesum  24443  measvuni  24560  sitgclg  24648  dmgmn0  24802  dmgmaddnn0  24803  dmgmdivn0  24804  lgamgulmlem2  24806  lgamgulmlem3  24807  lgamgulmlem5  24809  lgamgulmlem6  24810  lgamgulm2  24812  lgambdd  24813  lgamucov  24814  lgamcvg2  24831  gamcvg  24832  gamcvg2lem  24835  iprodgam  25311  rrndstprj2  26521  qirropth  26952  rmxyneg  26964  rmxm1  26978  rmxluc  26980  rmxdbl  26983  ltrmxnn0  26995  jm2.19lem1  27041  jm2.23  27048  rmxdiophlem  27067  aomclem2  27111  frlmssuvc2  27205  pmtrfinv  27360  symggen  27369  climrec  27686  climdivf  27695  stoweidlem34  27740  stoweidlem43  27749  lsatelbN  29731  lsatfixedN  29734  lkreqN  29895  lkrlspeqN  29896  dochnel2  32117  dochnel  32118  djhcvat42  32140  dochsnshp  32178  dochexmidat  32184  dochsnkr  32197  dochsnkr2  32198  dochsnkr2cl  32199  dochflcl  32200  dochfl1  32201  dochfln0  32202  lcfl6lem  32223  lcfl7lem  32224  lcfl8b  32229  lclkrlem2a  32232  lclkrlem2b  32233  lclkrlem2c  32234  lclkrlem2d  32235  lclkrlem2e  32236  lclkrlem2f  32237  lcfrlem14  32281  lcfrlem15  32282  lcfrlem16  32283  lcfrlem17  32284  lcfrlem18  32285  lcfrlem19  32286  lcfrlem20  32287  lcfrlem21  32288  lcfrlem23  32290  lcfrlem25  32292  lcfrlem26  32293  lcfrlem35  32302  lcfrlem36  32303  mapdn0  32394  mapdpglem29  32425  mapdpglem24  32429  baerlem3lem1  32432  baerlem5alem1  32433  baerlem5blem1  32434  baerlem3lem2  32435  baerlem5alem2  32436  baerlem5blem2  32437  baerlem5amN  32441  baerlem5bmN  32442  baerlem5abmN  32443  mapdindp0  32444  mapdindp1  32445  mapdindp2  32446  mapdindp3  32447  mapdindp4  32448  mapdheq2  32454  mapdheq4lem  32456  mapdheq4  32457  mapdh6lem1N  32458  mapdh6lem2N  32459  mapdh6aN  32460  mapdh6bN  32462  mapdh6cN  32463  mapdh6dN  32464  mapdh6eN  32465  mapdh6fN  32466  mapdh6gN  32467  mapdh6hN  32468  mapdh6iN  32469  mapdh7eN  32473  mapdh7cN  32474  mapdh7dN  32475  mapdh7fN  32476  mapdh75e  32477  mapdh75fN  32480  hvmaplfl  32492  mapdhvmap  32494  mapdh8aa  32501  mapdh8ab  32502  mapdh8ad  32504  mapdh8b  32505  mapdh8c  32506  mapdh8d0N  32507  mapdh8d  32508  mapdh8e  32509  mapdh9a  32515  hdmap1val2  32526  hdmap1eq  32527  hdmap1valc  32529  hdmap1eq2  32531  hdmap1eq4N  32532  hdmap1l6lem1  32533  hdmap1l6lem2  32534  hdmap1l6a  32535  hdmap1l6b  32537  hdmap1l6c  32538  hdmap1l6d  32539  hdmap1l6e  32540  hdmap1l6f  32541  hdmap1l6g  32542  hdmap1l6h  32543  hdmap1l6i  32544  hdmap1eulem  32549  hdmap1neglem1N  32553  hdmapcl  32558  hdmapval2lem  32559  hdmapval0  32561  hdmapeveclem  32562  hdmapevec  32563  hdmapval3lemN  32565  hdmapval3N  32566  hdmap10lem  32567  hdmap11lem1  32569  hdmap11lem2  32570  hdmapnzcl  32573  hdmaprnlem3N  32578  hdmaprnlem3uN  32579  hdmaprnlem4N  32581  hdmaprnlem7N  32583  hdmaprnlem8N  32584  hdmaprnlem9N  32585  hdmaprnlem3eN  32586  hdmaprnlem16N  32590  hdmap14lem1  32596  hdmap14lem2N  32597  hdmap14lem3  32598  hdmap14lem4a  32599  hdmap14lem6  32601  hdmap14lem8  32603  hdmap14lem9  32604  hdmap14lem10  32605  hdmap14lem11  32606  hdmap14lem12  32607  hgmaprnlem1N  32624  hgmaprnlem2N  32625  hgmaprnlem3N  32626  hgmaprnlem4N  32627  hdmapip1  32644  hdmapinvlem1  32646  hdmapinvlem2  32647  hdmapinvlem3  32648  hdmapinvlem4  32649  hdmapglem5  32650  hgmapvvlem1  32651  hgmapvvlem2  32652  hgmapvvlem3  32653  hdmapglem7a  32655  hdmapglem7b  32656  hdmapglem7  32657
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-v 2950  df-dif 3315
  Copyright terms: Public domain W3C validator