MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  difin Unicode version

Theorem difin 3734
Description: Difference with intersection. Theorem 33 of [Suppes] p. 29. (Contributed by NM, 31-Mar-1998.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
Assertion
Ref Expression
difin

Proof of Theorem difin
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 pm4.61 426 . . 3
2 anclb 547 . . . . 5
3 elin 3686 . . . . . 6
43imbi2i 312 . . . . 5
5 iman 424 . . . . 5
62, 4, 53bitr2i 273 . . . 4
76con2bii 332 . . 3
8 eldif 3485 . . 3
91, 7, 83bitr4i 277 . 2
109difeqri 3623 1
Colors of variables: wff setvar class
Syntax hints:  -.wn 3  ->wi 4  /\wa 369  =wceq 1395  e.wcel 1818  \cdif 3472  i^icin 3474
This theorem is referenced by:  dfin4  3737  indif  3739  symdif1  3762  notrab  3774  dfsdom2  7660  hashdif  12476  isercolllem3  13489  iuncld  19546  llycmpkgen2  20051  1stckgen  20055  ptbasfi  20082  txkgen  20153  cmmbl  21945  disjdifprg2  27437  onint1  29914  nzprmdif  31224  dvmptfprodlem  31741  bj-disjdif  34511
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-v 3111  df-dif 3478  df-in 3482
  Copyright terms: Public domain W3C validator