MPE Home 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  |-  ( A  u.  B )  =  ( _V  \  (
( _V  \  A
)  \  B )
)

Proof of Theorem dfun2
Dummy variable  x is distinct from all other variables.
StepHypRef Expression
1 vex 3084 . . . . . . 7  |-  x  e. 
_V
2 eldif 3446 . . . . . . 7  |-  ( x  e.  ( _V  \  A )  <->  ( x  e.  _V  /\  -.  x  e.  A ) )
31, 2mpbiran 926 . . . . . 6  |-  ( x  e.  ( _V  \  A )  <->  -.  x  e.  A )
43anbi1i 699 . . . . 5  |-  ( ( x  e.  ( _V 
\  A )  /\  -.  x  e.  B
)  <->  ( -.  x  e.  A  /\  -.  x  e.  B ) )
5 eldif 3446 . . . . 5  |-  ( x  e.  ( ( _V 
\  A )  \  B )  <->  ( x  e.  ( _V  \  A
)  /\  -.  x  e.  B ) )
6 ioran 492 . . . . 5  |-  ( -.  ( x  e.  A  \/  x  e.  B
)  <->  ( -.  x  e.  A  /\  -.  x  e.  B ) )
74, 5, 63bitr4i 280 . . . 4  |-  ( x  e.  ( ( _V 
\  A )  \  B )  <->  -.  (
x  e.  A  \/  x  e.  B )
)
87con2bii 333 . . 3  |-  ( ( x  e.  A  \/  x  e.  B )  <->  -.  x  e.  ( ( _V  \  A ) 
\  B ) )
9 eldif 3446 . . . 4  |-  ( x  e.  ( _V  \ 
( ( _V  \  A )  \  B
) )  <->  ( x  e.  _V  /\  -.  x  e.  ( ( _V  \  A )  \  B
) ) )
101, 9mpbiran 926 . . 3  |-  ( x  e.  ( _V  \ 
( ( _V  \  A )  \  B
) )  <->  -.  x  e.  ( ( _V  \  A )  \  B
) )
118, 10bitr4i 255 . 2  |-  ( ( x  e.  A  \/  x  e.  B )  <->  x  e.  ( _V  \ 
( ( _V  \  A )  \  B
) ) )
1211uneqri 3608 1  |-  ( A  u.  B )  =  ( _V  \  (
( _V  \  A
)  \  B )
)
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    \/ wo 369    /\ wa 370    = wceq 1437    e. wcel 1868   _Vcvv 3081    \ cdif 3433    u. 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