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

Theorem eldifbd 3620
Description: If a class is in the difference of two classes, it is not in the subtrahend. One-way deduction form of eldif 3617. (Contributed by David Moews, 1-May-2017.)
Hypothesis
Ref Expression
eldifbd.1 (𝜑𝐴 ∈ (𝐵𝐶))
Assertion
Ref Expression
eldifbd (𝜑 → ¬ 𝐴𝐶)

Proof of Theorem eldifbd
StepHypRef Expression
1 eldifbd.1 . . 3 (𝜑𝐴 ∈ (𝐵𝐶))
2 eldif 3617 . . 3 (𝐴 ∈ (𝐵𝐶) ↔ (𝐴𝐵 ∧ ¬ 𝐴𝐶))
31, 2sylib 208 . 2 (𝜑 → (𝐴𝐵 ∧ ¬ 𝐴𝐶))
43simprd 478 1 (𝜑 → ¬ 𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 383  wcel 2030  cdif 3604
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-v 3233  df-dif 3610
This theorem is referenced by:  xpdifid  5597  boxcutc  7993  infeq5i  8571  cantnflem2  8625  ackbij1lem18  9097  infpssrlem4  9166  fin23lem30  9202  domtriomlem  9302  pwfseqlem4  9522  dvdsaddre2b  15076  dprdfadd  18465  pgpfac1lem2  18520  pgpfac1lem3a  18521  pgpfac1lem3  18522  lspsolv  19191  lsppratlem3  19197  mplsubrglem  19487  frlmssuvc2  20182  hauscmplem  21257  1stccnp  21313  1stckgen  21405  alexsublem  21895  bcthlem4  23170  plyeq0lem  24011  ftalem3  24846  tglngne  25490  1loopgrvd0  26456  disjiunel  29535  ofpreima2  29594  qqhval2  30154  esum2dlem  30282  carsgclctunlem1  30507  sibfof  30530  sitgaddlemb  30538  eulerpartlemsv2  30548  eulerpartlemv  30554  eulerpartlemgs2  30570  dochnel2  36998  rmspecnonsq  37789  disjiun2  39540  dstregt0  39807  fprodexp  40144  fprodabs2  40145  fprodcnlem  40149  lptre2pt  40190  dvnprodlem2  40480  stoweidlem43  40578  fourierdlem66  40707  hsphoidmvle2  41120  hsphoidmvle  41121  hoidmvlelem1  41130  hoidmvlelem2  41131  hoidmvlelem3  41132  hoidmvlelem4  41133
  Copyright terms: Public domain W3C validator