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

Theorem eldifbd 3962
Description: If a class is in the difference of two classes, it is not in the subtrahend. One-way deduction form of eldif 3959. (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 3959 . . 3 (𝐴 ∈ (𝐵𝐶) ↔ (𝐴𝐵 ∧ ¬ 𝐴𝐶))
31, 2sylib 217 . 2 (𝜑 → (𝐴𝐵 ∧ ¬ 𝐴𝐶))
43simprd 497 1 (𝜑 → ¬ 𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 397  wcel 2107  cdif 3946
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-dif 3952
This theorem is referenced by:  xpdifid  6168  boxcutc  8935  infeq5i  9631  cantnflem2  9685  ackbij1lem18  10232  infpssrlem4  10301  fin23lem30  10337  domtriomlem  10437  pwfseqlem4  10657  dvdsaddre2b  16250  dprdfadd  19890  pgpfac1lem2  19945  pgpfac1lem3a  19946  pgpfac1lem3  19947  lspsolv  20756  lsppratlem3  20762  frlmssuvc2  21350  mplsubrglem  21563  hauscmplem  22910  1stccnp  22966  1stckgen  23058  alexsublem  23548  bcthlem4  24844  plyeq0lem  25724  ftalem3  26579  tglngne  27801  1loopgrvd0  28761  disjiunel  31827  ofpreima2  31891  fvdifsupp  31907  nn0difffzod  32016  cycpmco2f1  32283  cycpmco2lem1  32285  cycpmco2lem5  32289  cycpmco2  32292  cyc3co2  32299  tocyccntz  32303  elrspunsn  32547  mxidlmaxv  32584  mxidlirredi  32587  qsdrnglem2  32610  gsummoncoe1fzo  32668  fedgmullem2  32715  qqhval2  32962  esum2dlem  33090  carsgclctunlem1  33316  sibfof  33339  sitgaddlemb  33347  eulerpartlemsv2  33357  eulerpartlemv  33363  eulerpartlemgs2  33379  dochnel2  40263  nelsubginvcld  41070  nelsubgcld  41071  fltne  41386  rmspecnonsq  41645  disjiun2  43745  dstregt0  43991  fprodexp  44310  fprodabs2  44311  fprodcnlem  44315  lptre2pt  44356  dvnprodlem2  44663  stoweidlem43  44759  fourierdlem66  44888  iundjiunlem  45175  hsphoidmvle2  45301  hsphoidmvle  45302  hoidmvlelem1  45311  hoidmvlelem2  45312  hoidmvlelem3  45313  hoidmvlelem4  45314  readdcnnred  46011  resubcnnred  46012  recnmulnred  46013  cndivrenred  46014
  Copyright terms: Public domain W3C validator