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

Theorem dfin4 3682
Description: Alternate definition of the intersection of two classes. Exercise 4.10(q) of [Mendelson] p. 231. (Contributed by NM, 25-Nov-2003.)
Assertion
Ref Expression
dfin4  |-  ( A  i^i  B )  =  ( A  \  ( A  \  B ) )

Proof of Theorem dfin4
StepHypRef Expression
1 inss1 3651 . . 3  |-  ( A  i^i  B )  C_  A
2 dfss4 3676 . . 3  |-  ( ( A  i^i  B ) 
C_  A  <->  ( A  \  ( A  \  ( A  i^i  B ) ) )  =  ( A  i^i  B ) )
31, 2mpbi 212 . 2  |-  ( A 
\  ( A  \ 
( A  i^i  B
) ) )  =  ( A  i^i  B
)
4 difin 3679 . . 3  |-  ( A 
\  ( A  i^i  B ) )  =  ( A  \  B )
54difeq2i 3547 . 2  |-  ( A 
\  ( A  \ 
( A  i^i  B
) ) )  =  ( A  \  ( A  \  B ) )
63, 5eqtr3i 2474 1  |-  ( A  i^i  B )  =  ( A  \  ( A  \  B ) )
Colors of variables: wff setvar class
Syntax hints:    = wceq 1443    \ cdif 3400    i^i cin 3402    C_ wss 3403
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1668  ax-4 1681  ax-5 1757  ax-6 1804  ax-7 1850  ax-10 1914  ax-11 1919  ax-12 1932  ax-13 2090  ax-ext 2430
This theorem depends on definitions:  df-bi 189  df-an 373  df-tru 1446  df-ex 1663  df-nf 1667  df-sb 1797  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2580  df-ral 2741  df-rab 2745  df-v 3046  df-dif 3406  df-in 3410  df-ss 3417
This theorem is referenced by:  indif  3684  cnvin  5242  imain  5657  resin  5833  elcls  20082  cmmbl  22481  mbfeqalem  22591  itg1addlem4  22650  itg1addlem5  22651  inelsiga  28950  inelros  28988  topdifinffinlem  31743  poimirlem9  31942  mblfinlem4  31973  ismblfin  31974  cnambfre  31982  stoweidlem50  37905  saliincl  38180  sge0fodjrnlem  38252  meadjiunlem  38297  caragendifcl  38329
  Copyright terms: Public domain W3C validator