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

Theorem eldifbd 3928
Description: If a class is in the difference of two classes, it is not in the subtrahend. One-way deduction form of eldif 3925. (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 3925 . . 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 3912
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 2708
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-v 3450  df-dif 3918
This theorem is referenced by:  xpdifid  6125  boxcutc  8886  infeq5i  9579  cantnflem2  9633  ackbij1lem18  10180  infpssrlem4  10249  fin23lem30  10285  domtriomlem  10385  pwfseqlem4  10605  dvdsaddre2b  16196  dprdfadd  19806  pgpfac1lem2  19861  pgpfac1lem3a  19862  pgpfac1lem3  19863  lspsolv  20620  lsppratlem3  20626  frlmssuvc2  21217  mplsubrglem  21426  hauscmplem  22773  1stccnp  22829  1stckgen  22921  alexsublem  23411  bcthlem4  24707  plyeq0lem  25587  ftalem3  26440  tglngne  27534  1loopgrvd0  28494  disjiunel  31556  ofpreima2  31624  fvdifsupp  31641  cycpmco2f1  32015  cycpmco2lem1  32017  cycpmco2lem5  32021  cycpmco2  32024  cyc3co2  32031  tocyccntz  32035  fedgmullem2  32365  qqhval2  32603  esum2dlem  32731  carsgclctunlem1  32957  sibfof  32980  sitgaddlemb  32988  eulerpartlemsv2  32998  eulerpartlemv  33004  eulerpartlemgs2  33020  dochnel2  39884  nelsubginvcld  40700  nelsubgcld  40701  fltne  41011  rmspecnonsq  41259  disjiun2  43340  dstregt0  43589  fprodexp  43909  fprodabs2  43910  fprodcnlem  43914  lptre2pt  43955  dvnprodlem2  44262  stoweidlem43  44358  fourierdlem66  44487  iundjiunlem  44774  hsphoidmvle2  44900  hsphoidmvle  44901  hoidmvlelem1  44910  hoidmvlelem2  44911  hoidmvlelem3  44912  hoidmvlelem4  44913  readdcnnred  45609  resubcnnred  45610  recnmulnred  45611  cndivrenred  45612
  Copyright terms: Public domain W3C validator