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

Theorem dfin2 3418
Description: An alternate definition of the intersection of two classes in terms of class difference, requiring no dummy variables. See comments under dfun2 3417. Another version is given by dfin4 3422. (Contributed by NM, 10-Jun-2004.)
Assertion
Ref Expression
dfin2  |-  ( A  i^i  B )  =  ( A  \  ( _V  \  B ) )

Proof of Theorem dfin2
Dummy variable  x is distinct from all other variables.
StepHypRef Expression
1 vex 2804 . . . . . 6  |-  x  e. 
_V
2 eldif 3175 . . . . . 6  |-  ( x  e.  ( _V  \  B )  <->  ( x  e.  _V  /\  -.  x  e.  B ) )
31, 2mpbiran 884 . . . . 5  |-  ( x  e.  ( _V  \  B )  <->  -.  x  e.  B )
43con2bii 322 . . . 4  |-  ( x  e.  B  <->  -.  x  e.  ( _V  \  B
) )
54anbi2i 675 . . 3  |-  ( ( x  e.  A  /\  x  e.  B )  <->  ( x  e.  A  /\  -.  x  e.  ( _V  \  B ) ) )
6 eldif 3175 . . 3  |-  ( x  e.  ( A  \ 
( _V  \  B
) )  <->  ( x  e.  A  /\  -.  x  e.  ( _V  \  B
) ) )
75, 6bitr4i 243 . 2  |-  ( ( x  e.  A  /\  x  e.  B )  <->  x  e.  ( A  \ 
( _V  \  B
) ) )
87ineqri 3375 1  |-  ( A  i^i  B )  =  ( A  \  ( _V  \  B ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    /\ wa 358    = wceq 1632    e. wcel 1696   _Vcvv 2801    \ cdif 3162    i^i cin 3164
This theorem is referenced by:  dfun3  3420  dfin3  3421  invdif  3423  difundi  3434  difindi  3436
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-v 2803  df-dif 3168  df-in 3172
  Copyright terms: Public domain W3C validator