Metamath Proof Explorer


Theorem difrab

Description: Difference of two restricted class abstractions. (Contributed by NM, 23-Oct-2004)

Ref Expression
Assertion difrab
|- ( { x e. A | ph } \ { x e. A | ps } ) = { x e. A | ( ph /\ -. ps ) }

Proof

Step Hyp Ref Expression
1 df-rab
 |-  { x e. A | ph } = { x | ( x e. A /\ ph ) }
2 df-rab
 |-  { x e. A | ps } = { x | ( x e. A /\ ps ) }
3 1 2 difeq12i
 |-  ( { x e. A | ph } \ { x e. A | ps } ) = ( { x | ( x e. A /\ ph ) } \ { x | ( x e. A /\ ps ) } )
4 df-rab
 |-  { x e. A | ( ph /\ -. ps ) } = { x | ( x e. A /\ ( ph /\ -. ps ) ) }
5 difab
 |-  ( { x | ( x e. A /\ ph ) } \ { x | ( x e. A /\ ps ) } ) = { x | ( ( x e. A /\ ph ) /\ -. ( x e. A /\ ps ) ) }
6 anass
 |-  ( ( ( x e. A /\ ph ) /\ -. ps ) <-> ( x e. A /\ ( ph /\ -. ps ) ) )
7 simpr
 |-  ( ( x e. A /\ ps ) -> ps )
8 7 con3i
 |-  ( -. ps -> -. ( x e. A /\ ps ) )
9 8 anim2i
 |-  ( ( ( x e. A /\ ph ) /\ -. ps ) -> ( ( x e. A /\ ph ) /\ -. ( x e. A /\ ps ) ) )
10 pm3.2
 |-  ( x e. A -> ( ps -> ( x e. A /\ ps ) ) )
11 10 adantr
 |-  ( ( x e. A /\ ph ) -> ( ps -> ( x e. A /\ ps ) ) )
12 11 con3d
 |-  ( ( x e. A /\ ph ) -> ( -. ( x e. A /\ ps ) -> -. ps ) )
13 12 imdistani
 |-  ( ( ( x e. A /\ ph ) /\ -. ( x e. A /\ ps ) ) -> ( ( x e. A /\ ph ) /\ -. ps ) )
14 9 13 impbii
 |-  ( ( ( x e. A /\ ph ) /\ -. ps ) <-> ( ( x e. A /\ ph ) /\ -. ( x e. A /\ ps ) ) )
15 6 14 bitr3i
 |-  ( ( x e. A /\ ( ph /\ -. ps ) ) <-> ( ( x e. A /\ ph ) /\ -. ( x e. A /\ ps ) ) )
16 15 abbii
 |-  { x | ( x e. A /\ ( ph /\ -. ps ) ) } = { x | ( ( x e. A /\ ph ) /\ -. ( x e. A /\ ps ) ) }
17 5 16 eqtr4i
 |-  ( { x | ( x e. A /\ ph ) } \ { x | ( x e. A /\ ps ) } ) = { x | ( x e. A /\ ( ph /\ -. ps ) ) }
18 4 17 eqtr4i
 |-  { x e. A | ( ph /\ -. ps ) } = ( { x | ( x e. A /\ ph ) } \ { x | ( x e. A /\ ps ) } )
19 3 18 eqtr4i
 |-  ( { x e. A | ph } \ { x e. A | ps } ) = { x e. A | ( ph /\ -. ps ) }