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

Theorem eldifad 3552
Description: If a class is in the difference of two classes, it is also in the minuend. One-way deduction form of eldif 3550. (Contributed by David Moews, 1-May-2017.)
Hypothesis
Ref Expression
eldifad.1 (𝜑𝐴 ∈ (𝐵𝐶))
Assertion
Ref Expression
eldifad (𝜑𝐴𝐵)

Proof of Theorem eldifad
StepHypRef Expression
1 eldifad.1 . . 3 (𝜑𝐴 ∈ (𝐵𝐶))
2 eldif 3550 . . 3 (𝐴 ∈ (𝐵𝐶) ↔ (𝐴𝐵 ∧ ¬ 𝐴𝐶))
31, 2sylib 207 . 2 (𝜑 → (𝐴𝐵 ∧ ¬ 𝐴𝐶))
43simpld 474 1 (𝜑𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 383  wcel 1977  cdif 3537
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-dif 3543
This theorem is referenced by:  xpdifid  5481  unblem1  8097  cantnflem3  8471  cantnflem4  8472  oef1o  8478  infxpenc  8724  acndom2  8760  ackbij1lem18  8942  infpssrlem3  9010  fin23lem26  9030  fin23lem30  9047  pwfseqlem4a  9362  expclz  12747  symgextf  17660  pmtrfinv  17704  symggen  17713  efgsdmi  17968  efgs1b  17972  efgsp1  17973  efgsres  17974  efgredlemf  17977  efgredlemd  17980  efgredlem  17983  efgrelexlemb  17986  gsum2d2lem  18195  pgpfac1lem2  18297  pgpfac1lem3a  18298  pgpfac1lem3  18299  pgpfac1lem4  18300  isdrng2  18580  lvecinv  18934  lspsncmp  18937  lspsnne1  18938  lspsnnecom  18940  lspabs2  18941  lspsneu  18944  lspdisjb  18947  lspexch  18950  lspindp1  18954  lvecindp2  18960  lspsolv  18964  lspsnat  18966  lsppratlem1  18968  lsppratlem2  18969  fidomndrnglem  19127  frlmssuvc2  19953  maducoeval2  20265  hauscmplem  21019  1stccnp  21075  imasdsf1olem  21988  rrxmetlem  22998  dvrec  23524  ftc1lem6  23608  elqaalem1  23878  elqaalem3  23880  ulmdvlem3  23960  abelthlem6  23994  abelthlem7a  23995  abelthlem7  23996  logtayl  24206  dmgmn0  24552  dmgmaddnn0  24553  dmgmdivn0  24554  lgamgulmlem2  24556  lgamgulmlem3  24557  lgamgulmlem5  24559  lgamgulmlem6  24560  lgamgulm2  24562  lgambdd  24563  lgamucov  24564  lgamcvg2  24581  gamcvg  24582  gamcvg2lem  24585  ftalem3  24601  lgsqrlem1  24871  lgsqrlem2  24872  lgsqrlem3  24873  lgsqrlem4  24874  lgseisenlem1  24900  lgseisenlem2  24901  lgseisenlem3  24902  lgseisenlem4  24903  lgseisen  24904  lgsquadlem2  24906  lgsquadlem3  24907  chebbnd1lem1  24958  dchrisum0re  25002  dchrisum0lema  25003  dchrisum0lem1b  25004  dchrisum0lem1  25005  dchrisum0lem2a  25006  dchrisum0lem2  25007  tgisline  25322  elntg  25664  uhgrss  25730  upgrex  25759  edguhgr  25803  uhgrass  25835  umgraex  25852  disjiunel  28791  submatminr1  29204  qtophaus  29231  qqhval2  29354  esummono  29443  gsumesum  29448  esum2dlem  29481  measvuni  29604  fiunelcarsg  29705  sitgclg  29731  sitgaddlemb  29737  eulerpartlemsv2  29747  eulerpartlemsv3  29750  eulerpartlemgc  29751  eulerpartlemv  29753  signstfvneq0  29975  signstfvcl  29976  signstfveq0a  29979  signstfveq0  29980  signsvfn  29985  signsvtp  29986  signsvtn  29987  signsvfpn  29988  signsvfnn  29989  signlem0  29990  iprodgam  30881  poimirlem2  32581  rrndstprj2  32800  lsatelbN  33311  lsatfixedN  33314  lkreqN  33475  lkrlspeqN  33476  dochnel2  35699  dochnel  35700  djhcvat42  35722  dochsnshp  35760  dochexmidat  35766  dochsnkr  35779  dochsnkr2  35780  dochsnkr2cl  35781  dochflcl  35782  dochfl1  35783  dochfln0  35784  lcfl6lem  35805  lcfl7lem  35806  lcfl8b  35811  lclkrlem2a  35814  lclkrlem2b  35815  lclkrlem2c  35816  lclkrlem2d  35817  lclkrlem2e  35818  lclkrlem2f  35819  lcfrlem14  35863  lcfrlem15  35864  lcfrlem16  35865  lcfrlem17  35866  lcfrlem18  35867  lcfrlem19  35868  lcfrlem20  35869  lcfrlem21  35870  lcfrlem23  35872  lcfrlem25  35874  lcfrlem26  35875  lcfrlem35  35884  lcfrlem36  35885  mapdn0  35976  mapdpglem29  36007  mapdpglem24  36011  baerlem3lem1  36014  baerlem5alem1  36015  baerlem5blem1  36016  baerlem3lem2  36017  baerlem5alem2  36018  baerlem5blem2  36019  baerlem5amN  36023  baerlem5bmN  36024  baerlem5abmN  36025  mapdindp0  36026  mapdindp1  36027  mapdindp2  36028  mapdindp3  36029  mapdindp4  36030  mapdheq2  36036  mapdheq4lem  36038  mapdheq4  36039  mapdh6lem1N  36040  mapdh6lem2N  36041  mapdh6aN  36042  mapdh6bN  36044  mapdh6cN  36045  mapdh6dN  36046  mapdh6eN  36047  mapdh6fN  36048  mapdh6gN  36049  mapdh6hN  36050  mapdh6iN  36051  mapdh7eN  36055  mapdh7cN  36056  mapdh7dN  36057  mapdh7fN  36058  mapdh75e  36059  mapdh75fN  36062  hvmaplfl  36074  mapdhvmap  36076  mapdh8aa  36083  mapdh8ab  36084  mapdh8ad  36086  mapdh8b  36087  mapdh8c  36088  mapdh8d0N  36089  mapdh8d  36090  mapdh8e  36091  mapdh9a  36097  mapdh9aOLDN  36098  hdmap1val2  36108  hdmap1eq  36109  hdmap1valc  36111  hdmap1eq2  36113  hdmap1eq4N  36114  hdmap1l6lem1  36115  hdmap1l6lem2  36116  hdmap1l6a  36117  hdmap1l6b  36119  hdmap1l6c  36120  hdmap1l6d  36121  hdmap1l6e  36122  hdmap1l6f  36123  hdmap1l6g  36124  hdmap1l6h  36125  hdmap1l6i  36126  hdmap1eulem  36131  hdmap1eulemOLDN  36132  hdmap1neglem1N  36135  hdmapcl  36140  hdmapval2lem  36141  hdmapval0  36143  hdmapeveclem  36144  hdmapevec  36145  hdmapval3lemN  36147  hdmapval3N  36148  hdmap10lem  36149  hdmap11lem1  36151  hdmap11lem2  36152  hdmapnzcl  36155  hdmaprnlem3N  36160  hdmaprnlem3uN  36161  hdmaprnlem4N  36163  hdmaprnlem7N  36165  hdmaprnlem8N  36166  hdmaprnlem9N  36167  hdmaprnlem3eN  36168  hdmaprnlem16N  36172  hdmap14lem1  36178  hdmap14lem2N  36179  hdmap14lem3  36180  hdmap14lem4a  36181  hdmap14lem6  36183  hdmap14lem8  36185  hdmap14lem9  36186  hdmap14lem10  36187  hdmap14lem11  36188  hdmap14lem12  36189  hgmaprnlem1N  36206  hgmaprnlem2N  36207  hgmaprnlem3N  36208  hgmaprnlem4N  36209  hdmapip1  36226  hdmapinvlem1  36228  hdmapinvlem2  36229  hdmapinvlem3  36230  hdmapinvlem4  36231  hdmapglem5  36232  hgmapvvlem1  36233  hgmapvvlem2  36234  hgmapvvlem3  36235  hdmapglem7a  36237  hdmapglem7b  36238  hdmapglem7  36239  qirropth  36491  rmxyneg  36503  rmxm1  36517  rmxluc  36519  rmxdbl  36522  ltrmxnn0  36534  jm2.19lem1  36574  jm2.23  36581  rmxdiophlem  36600  aomclem2  36643  bccm1k  37563  dstregt0  38434  fprodexp  38661  fprodabs2  38662  mccllem  38664  fprodcnlem  38666  climrec  38670  climdivf  38679  islpcn  38706  lptre2pt  38707  0ellimcdiv  38716  reclimc  38720  divlimc  38723  divcncf  38769  cncficcgt0  38774  dvmptdiv  38807  dvdivf  38812  stoweidlem34  38927  stoweidlem43  38936  etransclem46  39173  etransclem47  39174  etransclem48  39175  hsphoidmvle2  39475  hsphoidmvle  39476  hoidmvlelem3  39487  hoidmvlelem4  39488  hspdifhsp  39506  1loopgrvd0  40719  zrzeroorngc  41794  zrtermoringc  41862  zrninitoringc  41863  nzerooringczr  41864
  Copyright terms: Public domain W3C validator