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

Theorem dfun2 3512
Description: An alternate definition of the union of two classes in terms of class difference, requiring no dummy variables. Along with dfin2 3513 and dfss4 3511 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 2895 . . . . . . 7  |-  x  e. 
_V
2 eldif 3266 . . . . . . 7  |-  ( x  e.  ( _V  \  A )  <->  ( x  e.  _V  /\  -.  x  e.  A ) )
31, 2mpbiran 885 . . . . . 6  |-  ( x  e.  ( _V  \  A )  <->  -.  x  e.  A )
43anbi1i 677 . . . . 5  |-  ( ( x  e.  ( _V 
\  A )  /\  -.  x  e.  B
)  <->  ( -.  x  e.  A  /\  -.  x  e.  B ) )
5 eldif 3266 . . . . 5  |-  ( x  e.  ( ( _V 
\  A )  \  B )  <->  ( x  e.  ( _V  \  A
)  /\  -.  x  e.  B ) )
6 ioran 477 . . . . 5  |-  ( -.  ( x  e.  A  \/  x  e.  B
)  <->  ( -.  x  e.  A  /\  -.  x  e.  B ) )
74, 5, 63bitr4i 269 . . . 4  |-  ( x  e.  ( ( _V 
\  A )  \  B )  <->  -.  (
x  e.  A  \/  x  e.  B )
)
87con2bii 323 . . 3  |-  ( ( x  e.  A  \/  x  e.  B )  <->  -.  x  e.  ( ( _V  \  A ) 
\  B ) )
9 eldif 3266 . . . 4  |-  ( x  e.  ( _V  \ 
( ( _V  \  A )  \  B
) )  <->  ( x  e.  _V  /\  -.  x  e.  ( ( _V  \  A )  \  B
) ) )
101, 9mpbiran 885 . . 3  |-  ( x  e.  ( _V  \ 
( ( _V  \  A )  \  B
) )  <->  -.  x  e.  ( ( _V  \  A )  \  B
) )
118, 10bitr4i 244 . 2  |-  ( ( x  e.  A  \/  x  e.  B )  <->  x  e.  ( _V  \ 
( ( _V  \  A )  \  B
) ) )
1211uneqri 3425 1  |-  ( A  u.  B )  =  ( _V  \  (
( _V  \  A
)  \  B )
)
Colors of variables: wff set class
Syntax hints:   -. wn 3    \/ wo 358    /\ wa 359    = wceq 1649    e. wcel 1717   _Vcvv 2892    \ cdif 3253    u. cun 3254
This theorem is referenced by:  dfun3  3515  dfin3  3516
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2361
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2367  df-cleq 2373  df-clel 2376  df-nfc 2505  df-v 2894  df-dif 3259  df-un 3261
  Copyright terms: Public domain W3C validator