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

Theorem dfun2 3708
 Description: An alternate definition of the union of two classes in terms of class difference, requiring no dummy variables. Along with dfin2 3709 and dfss4 3707 it shows we can express union, intersection, and subset directly in terms of the single "primitive" operation (class difference). (Contributed by NM, 10-Jun-2004.)
Assertion
Ref Expression
dfun2

Proof of Theorem dfun2
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 vex 3084 . . . . . . 7
2 eldif 3446 . . . . . . 7
31, 2mpbiran 926 . . . . . 6
43anbi1i 699 . . . . 5
5 eldif 3446 . . . . 5
6 ioran 492 . . . . 5
74, 5, 63bitr4i 280 . . . 4
87con2bii 333 . . 3
9 eldif 3446 . . . 4
101, 9mpbiran 926 . . 3
118, 10bitr4i 255 . 2
1211uneqri 3608 1
 Colors of variables: wff setvar class Syntax hints:   wn 3   wo 369   wa 370   wceq 1437   wcel 1868  cvv 3081   cdif 3433   cun 3434 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400 This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-v 3083  df-dif 3439  df-un 3441 This theorem is referenced by:  dfun3  3711  dfin3  3712
 Copyright terms: Public domain W3C validator