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

Theorem eldifbd 3905
Description: If a class is in the difference of two classes, it is not in the subtrahend. One-way deduction form of eldif 3902. (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 3902 . . 3 (𝐴 ∈ (𝐵𝐶) ↔ (𝐴𝐵 ∧ ¬ 𝐴𝐶))
31, 2sylib 217 . 2 (𝜑 → (𝐴𝐵 ∧ ¬ 𝐴𝐶))
43simprd 496 1 (𝜑 → ¬ 𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 396  wcel 2110  cdif 3889
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-8 2112  ax-9 2120  ax-ext 2711
This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1545  df-ex 1787  df-sb 2072  df-clab 2718  df-cleq 2732  df-clel 2818  df-v 3433  df-dif 3895
This theorem is referenced by:  xpdifid  6070  boxcutc  8712  infeq5i  9372  cantnflem2  9426  ackbij1lem18  9994  infpssrlem4  10063  fin23lem30  10099  domtriomlem  10199  pwfseqlem4  10419  dvdsaddre2b  16014  dprdfadd  19621  pgpfac1lem2  19676  pgpfac1lem3a  19677  pgpfac1lem3  19678  lspsolv  20403  lsppratlem3  20409  frlmssuvc2  21000  mplsubrglem  21208  hauscmplem  22555  1stccnp  22611  1stckgen  22703  alexsublem  23193  bcthlem4  24489  plyeq0lem  25369  ftalem3  26222  tglngne  26909  1loopgrvd0  27869  disjiunel  30931  ofpreima2  30999  fvdifsupp  31014  cycpmco2f1  31387  cycpmco2lem1  31389  cycpmco2lem5  31393  cycpmco2  31396  cyc3co2  31403  tocyccntz  31407  fedgmullem2  31707  qqhval2  31928  esum2dlem  32056  carsgclctunlem1  32280  sibfof  32303  sitgaddlemb  32311  eulerpartlemsv2  32321  eulerpartlemv  32327  eulerpartlemgs2  32343  dochnel2  39402  nelsubginvcld  40217  nelsubgcld  40218  fltne  40478  rmspecnonsq  40726  disjiun2  42576  dstregt0  42790  fprodexp  43106  fprodabs2  43107  fprodcnlem  43111  lptre2pt  43152  dvnprodlem2  43459  stoweidlem43  43555  fourierdlem66  43684  iundjiunlem  43968  hsphoidmvle2  44094  hsphoidmvle  44095  hoidmvlelem1  44104  hoidmvlelem2  44105  hoidmvlelem3  44106  hoidmvlelem4  44107  readdcnnred  44764  resubcnnred  44765  recnmulnred  44766  cndivrenred  44767
  Copyright terms: Public domain W3C validator