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

Theorem dfun2 3696
Description: An alternate definition of the union of two classes in terms of class difference, requiring no dummy variables. Along with dfin2 3697 and dfss4 3695 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 3081 . . . . . . 7  |-  x  e. 
_V
2 eldif 3449 . . . . . . 7  |-  ( x  e.  ( _V  \  A )  <->  ( x  e.  _V  /\  -.  x  e.  A ) )
31, 2mpbiran 909 . . . . . 6  |-  ( x  e.  ( _V  \  A )  <->  -.  x  e.  A )
43anbi1i 695 . . . . 5  |-  ( ( x  e.  ( _V 
\  A )  /\  -.  x  e.  B
)  <->  ( -.  x  e.  A  /\  -.  x  e.  B ) )
5 eldif 3449 . . . . 5  |-  ( x  e.  ( ( _V 
\  A )  \  B )  <->  ( x  e.  ( _V  \  A
)  /\  -.  x  e.  B ) )
6 ioran 490 . . . . 5  |-  ( -.  ( x  e.  A  \/  x  e.  B
)  <->  ( -.  x  e.  A  /\  -.  x  e.  B ) )
74, 5, 63bitr4i 277 . . . 4  |-  ( x  e.  ( ( _V 
\  A )  \  B )  <->  -.  (
x  e.  A  \/  x  e.  B )
)
87con2bii 332 . . 3  |-  ( ( x  e.  A  \/  x  e.  B )  <->  -.  x  e.  ( ( _V  \  A ) 
\  B ) )
9 eldif 3449 . . . 4  |-  ( x  e.  ( _V  \ 
( ( _V  \  A )  \  B
) )  <->  ( x  e.  _V  /\  -.  x  e.  ( ( _V  \  A )  \  B
) ) )
101, 9mpbiran 909 . . 3  |-  ( x  e.  ( _V  \ 
( ( _V  \  A )  \  B
) )  <->  -.  x  e.  ( ( _V  \  A )  \  B
) )
118, 10bitr4i 252 . 2  |-  ( ( x  e.  A  \/  x  e.  B )  <->  x  e.  ( _V  \ 
( ( _V  \  A )  \  B
) ) )
1211uneqri 3609 1  |-  ( A  u.  B )  =  ( _V  \  (
( _V  \  A
)  \  B )
)
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    \/ wo 368    /\ wa 369    = wceq 1370    e. wcel 1758   _Vcvv 3078    \ cdif 3436    u. cun 3437
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-v 3080  df-dif 3442  df-un 3444
This theorem is referenced by:  dfun3  3699  dfin3  3700
  Copyright terms: Public domain W3C validator