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

Theorem dfin2 3520
Description: An alternate definition of the intersection of two classes in terms of class difference, requiring no dummy variables. See comments under dfun2 3519. Another version is given by dfin4 3524. (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 2902 . . . . . 6  |-  x  e. 
_V
2 eldif 3273 . . . . . 6  |-  ( x  e.  ( _V  \  B )  <->  ( x  e.  _V  /\  -.  x  e.  B ) )
31, 2mpbiran 885 . . . . 5  |-  ( x  e.  ( _V  \  B )  <->  -.  x  e.  B )
43con2bii 323 . . . 4  |-  ( x  e.  B  <->  -.  x  e.  ( _V  \  B
) )
54anbi2i 676 . . 3  |-  ( ( x  e.  A  /\  x  e.  B )  <->  ( x  e.  A  /\  -.  x  e.  ( _V  \  B ) ) )
6 eldif 3273 . . 3  |-  ( x  e.  ( A  \ 
( _V  \  B
) )  <->  ( x  e.  A  /\  -.  x  e.  ( _V  \  B
) ) )
75, 6bitr4i 244 . 2  |-  ( ( x  e.  A  /\  x  e.  B )  <->  x  e.  ( A  \ 
( _V  \  B
) ) )
87ineqri 3477 1  |-  ( A  i^i  B )  =  ( A  \  ( _V  \  B ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    /\ wa 359    = wceq 1649    e. wcel 1717   _Vcvv 2899    \ cdif 3260    i^i cin 3262
This theorem is referenced by:  dfun3  3522  dfin3  3523  invdif  3525  difundi  3536  difindi  3538  difdif2  3541
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 2368
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 2374  df-cleq 2380  df-clel 2383  df-nfc 2512  df-v 2901  df-dif 3266  df-in 3270
  Copyright terms: Public domain W3C validator