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 relopabv
 |-  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 relopabv
 |-  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 ) }