Metamath Proof Explorer

Theorem difopab

Description: Difference of two ordered-pair class abstractions. (Contributed by Stefan O'Rear, 17-Jan-2015)

Ref Expression
Assertion difopab 
|- ( { <. x , y >. | ph } \ { <. x , y >. | ps } ) = { <. x , y >. | ( ph /\ -. ps ) }

Proof

Step Hyp Ref Expression
1 relopab 
 |-  Rel { <. x , y >. | ph }
2 reldif 
 |-  ( Rel { <. x , y >. | ph } -> Rel ( { <. x , y >. | ph } \ { <. x , y >. | ps } ) )
3 1 2 ax-mp 
 |-  Rel ( { <. x , y >. | ph } \ { <. x , y >. | ps } )
4 relopab 
 |-  Rel { <. x , y >. | ( ph /\ -. ps ) }
5 sbcan 
 |-  ( [. z / x ]. ( [. w / y ]. ph /\ [. w / y ]. -. ps ) <-> ( [. z / x ]. [. w / y ]. ph /\ [. z / x ]. [. w / y ]. -. ps ) )
6 sbcan 
 |-  ( [. w / y ]. ( ph /\ -. ps ) <-> ( [. w / y ]. ph /\ [. w / y ]. -. ps ) )
7 6 sbcbii 
 |-  ( [. z / x ]. [. w / y ]. ( ph /\ -. ps ) <-> [. z / x ]. ( [. w / y ]. ph /\ [. w / y ]. -. ps ) )
8 opelopabsb 
 |-  ( <. z , w >. e. { <. x , y >. | ph } <-> [. z / x ]. [. w / y ]. ph )
9 sbcng 
 |-  ( z e. _V -> ( [. z / x ]. -. [. w / y ]. ps <-> -. [. z / x ]. [. w / y ]. ps ) )
10 9 elv 
 |-  ( [. z / x ]. -. [. w / y ]. ps <-> -. [. z / x ]. [. w / y ]. ps )
11 sbcng 
 |-  ( w e. _V -> ( [. w / y ]. -. ps <-> -. [. w / y ]. ps ) )
12 11 elv 
 |-  ( [. w / y ]. -. ps <-> -. [. w / y ]. ps )
13 12 sbcbii 
 |-  ( [. z / x ]. [. w / y ]. -. ps <-> [. z / x ]. -. [. w / y ]. ps )
14 opelopabsb 
 |-  ( <. z , w >. e. { <. x , y >. | ps } <-> [. z / x ]. [. w / y ]. ps )
15 14 notbii 
 |-  ( -. <. z , w >. e. { <. x , y >. | ps } <-> -. [. z / x ]. [. w / y ]. ps )
16 10 13 15 3bitr4ri 
 |-  ( -. <. z , w >. e. { <. x , y >. | ps } <-> [. z / x ]. [. w / y ]. -. ps )
17 8 16 anbi12i 
 |-  ( ( <. z , w >. e. { <. x , y >. | ph } /\ -. <. z , w >. e. { <. x , y >. | ps } ) <-> ( [. z / x ]. [. w / y ]. ph /\ [. z / x ]. [. w / y ]. -. ps ) )
18 5 7 17 3bitr4ri 
 |-  ( ( <. z , w >. e. { <. x , y >. | ph } /\ -. <. z , w >. e. { <. x , y >. | ps } ) <-> [. z / x ]. [. w / y ]. ( ph /\ -. ps ) )
19 eldif 
 |-  ( <. z , w >. e. ( { <. x , y >. | ph } \ { <. x , y >. | ps } ) <-> ( <. z , w >. e. { <. x , y >. | ph } /\ -. <. z , w >. e. { <. x , y >. | ps } ) )
20 opelopabsb 
 |-  ( <. z , w >. e. { <. x , y >. | ( ph /\ -. ps ) } <-> [. z / x ]. [. w / y ]. ( ph /\ -. ps ) )
21 18 19 20 3bitr4i 
 |-  ( <. z , w >. e. ( { <. x , y >. | ph } \ { <. x , y >. | ps } ) <-> <. z , w >. e. { <. x , y >. | ( ph /\ -. ps ) } )
22 3 4 21 eqrelriiv 
 |-  ( { <. x , y >. | ph } \ { <. x , y >. | ps } ) = { <. x , y >. | ( ph /\ -. ps ) }