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

Theorem eldifbd 3728
 Description: If a class is in the difference of two classes, it is not in the subtrahend. One-way deduction form of eldif 3725. (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 3725 . . 3 (𝐴 ∈ (𝐵𝐶) ↔ (𝐴𝐵 ∧ ¬ 𝐴𝐶))
31, 2sylib 208 . 2 (𝜑 → (𝐴𝐵 ∧ ¬ 𝐴𝐶))
43simprd 482 1 (𝜑 → ¬ 𝐴𝐶)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 383   ∈ wcel 2139   ∖ cdif 3712 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-v 3342  df-dif 3718 This theorem is referenced by:  xpdifid  5720  boxcutc  8117  infeq5i  8706  cantnflem2  8760  ackbij1lem18  9251  infpssrlem4  9320  fin23lem30  9356  domtriomlem  9456  pwfseqlem4  9676  dvdsaddre2b  15231  dprdfadd  18619  pgpfac1lem2  18674  pgpfac1lem3a  18675  pgpfac1lem3  18676  lspsolv  19345  lsppratlem3  19351  mplsubrglem  19641  frlmssuvc2  20336  hauscmplem  21411  1stccnp  21467  1stckgen  21559  alexsublem  22049  bcthlem4  23324  plyeq0lem  24165  ftalem3  25000  tglngne  25644  1loopgrvd0  26610  disjiunel  29716  ofpreima2  29775  qqhval2  30335  esum2dlem  30463  carsgclctunlem1  30688  sibfof  30711  sitgaddlemb  30719  eulerpartlemsv2  30729  eulerpartlemv  30735  eulerpartlemgs2  30751  dochnel2  37183  rmspecnonsq  37974  disjiun2  39725  dstregt0  39992  fprodexp  40329  fprodabs2  40330  fprodcnlem  40334  lptre2pt  40375  dvnprodlem2  40665  stoweidlem43  40763  fourierdlem66  40892  hsphoidmvle2  41305  hsphoidmvle  41306  hoidmvlelem1  41315  hoidmvlelem2  41316  hoidmvlelem3  41317  hoidmvlelem4  41318
 Copyright terms: Public domain W3C validator