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

Theorem eldifbd 3897
Description: If a class is in the difference of two classes, it is not in the subtrahend. One-way deduction form of eldif 3894. (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 3894 . . 3 (𝐴 ∈ (𝐵𝐶) ↔ (𝐴𝐵 ∧ ¬ 𝐴𝐶))
31, 2sylib 221 . 2 (𝜑 → (𝐴𝐵 ∧ ¬ 𝐴𝐶))
43simprd 499 1 (𝜑 → ¬ 𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 399  wcel 2112  cdif 3881
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-ext 2773
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2780  df-cleq 2794  df-clel 2873  df-v 3446  df-dif 3887
This theorem is referenced by:  xpdifid  5996  boxcutc  8492  infeq5i  9087  cantnflem2  9141  ackbij1lem18  9652  infpssrlem4  9721  fin23lem30  9757  domtriomlem  9857  pwfseqlem4  10077  dvdsaddre2b  15653  dprdfadd  19139  pgpfac1lem2  19194  pgpfac1lem3a  19195  pgpfac1lem3  19196  lspsolv  19912  lsppratlem3  19918  frlmssuvc2  20488  mplsubrglem  20681  hauscmplem  22015  1stccnp  22071  1stckgen  22163  alexsublem  22653  bcthlem4  23935  plyeq0lem  24811  ftalem3  25664  tglngne  26348  1loopgrvd0  27298  disjiunel  30363  ofpreima2  30433  fvdifsupp  30448  cycpmco2f1  30820  cycpmco2lem1  30822  cycpmco2lem5  30826  cycpmco2  30829  cyc3co2  30836  tocyccntz  30840  fedgmullem2  31118  qqhval2  31337  esum2dlem  31465  carsgclctunlem1  31689  sibfof  31712  sitgaddlemb  31720  eulerpartlemsv2  31730  eulerpartlemv  31736  eulerpartlemgs2  31752  dochnel2  38687  nelsubginvcld  39416  nelsubgcld  39417  fltne  39609  rmspecnonsq  39841  disjiun2  41685  dstregt0  41905  fprodexp  42229  fprodabs2  42230  fprodcnlem  42234  lptre2pt  42275  dvnprodlem2  42582  stoweidlem43  42678  fourierdlem66  42807  iundjiunlem  43091  hsphoidmvle2  43217  hsphoidmvle  43218  hoidmvlelem1  43227  hoidmvlelem2  43228  hoidmvlelem3  43229  hoidmvlelem4  43230  readdcnnred  43853  resubcnnred  43854  recnmulnred  43855  cndivrenred  43856
  Copyright terms: Public domain W3C validator