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

Theorem dfin4 3713
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 3682 . . 3  |-  ( A  i^i  B )  C_  A
2 dfss4 3707 . . 3  |-  ( ( A  i^i  B ) 
C_  A  <->  ( A  \  ( A  \  ( A  i^i  B ) ) )  =  ( A  i^i  B ) )
31, 2mpbi 211 . 2  |-  ( A 
\  ( A  \ 
( A  i^i  B
) ) )  =  ( A  i^i  B
)
4 difin 3710 . . 3  |-  ( A 
\  ( A  i^i  B ) )  =  ( A  \  B )
54difeq2i 3580 . 2  |-  ( A 
\  ( A  \ 
( A  i^i  B
) ) )  =  ( A  \  ( A  \  B ) )
63, 5eqtr3i 2453 1  |-  ( A  i^i  B )  =  ( A  \  ( A  \  B ) )
Colors of variables: wff setvar class
Syntax hints:    = wceq 1437    \ cdif 3433    i^i cin 3435    C_ wss 3436
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-ral 2780  df-rab 2784  df-v 3083  df-dif 3439  df-in 3443  df-ss 3450
This theorem is referenced by:  indif  3715  cnvin  5258  imain  5673  resin  5848  elcls  20075  cmmbl  22474  mbfeqalem  22584  itg1addlem4  22643  itg1addlem5  22644  inelsiga  28952  inelros  28990  topdifinffinlem  31690  poimirlem9  31862  mblfinlem4  31893  ismblfin  31894  cnambfre  31902  stoweidlem50  37730  saliincl  37986  sge0fodjrnlem  38045  meadjiunlem  38081  caragendifcl  38113
  Copyright terms: Public domain W3C validator