Metamath Proof Explorer

Theorem difopab

Description: Difference of two ordered-pair class abstractions. (Contributed by Stefan O'Rear, 17-Jan-2015) (Proof shortened by SN, 19-Dec-2024)

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 sban 
 |-  ( [ z / x ] ( [ w / y ] ph /\ [ w / y ] -. ps ) <-> ( [ z / x ] [ w / y ] ph /\ [ z / x ] [ w / y ] -. ps ) )
6 sban 
 |-  ( [ w / y ] ( ph /\ -. ps ) <-> ( [ w / y ] ph /\ [ w / y ] -. ps ) )
7 6 sbbii 
 |-  ( [ z / x ] [ w / y ] ( ph /\ -. ps ) <-> [ z / x ] ( [ w / y ] ph /\ [ w / y ] -. ps ) )
8 vopelopabsb 
 |-  ( <. z , w >. e. { <. x , y >. | ph } <-> [ z / x ] [ w / y ] ph )
9 sbn 
 |-  ( [ z / x ] -. [ w / y ] ps <-> -. [ z / x ] [ w / y ] ps )
10 sbn 
 |-  ( [ w / y ] -. ps <-> -. [ w / y ] ps )
11 10 sbbii 
 |-  ( [ z / x ] [ w / y ] -. ps <-> [ z / x ] -. [ w / y ] ps )
12 vopelopabsb 
 |-  ( <. z , w >. e. { <. x , y >. | ps } <-> [ z / x ] [ w / y ] ps )
13 12 notbii 
 |-  ( -. <. z , w >. e. { <. x , y >. | ps } <-> -. [ z / x ] [ w / y ] ps )
14 9 11 13 3bitr4ri 
 |-  ( -. <. z , w >. e. { <. x , y >. | ps } <-> [ z / x ] [ w / y ] -. ps )
15 8 14 anbi12i 
 |-  ( ( <. z , w >. e. { <. x , y >. | ph } /\ -. <. z , w >. e. { <. x , y >. | ps } ) <-> ( [ z / x ] [ w / y ] ph /\ [ z / x ] [ w / y ] -. ps ) )
16 5 7 15 3bitr4ri 
 |-  ( ( <. z , w >. e. { <. x , y >. | ph } /\ -. <. z , w >. e. { <. x , y >. | ps } ) <-> [ z / x ] [ w / y ] ( ph /\ -. ps ) )
17 eldif 
 |-  ( <. z , w >. e. ( { <. x , y >. | ph } \ { <. x , y >. | ps } ) <-> ( <. z , w >. e. { <. x , y >. | ph } /\ -. <. z , w >. e. { <. x , y >. | ps } ) )
18 vopelopabsb 
 |-  ( <. z , w >. e. { <. x , y >. | ( ph /\ -. ps ) } <-> [ z / x ] [ w / y ] ( ph /\ -. ps ) )
19 16 17 18 3bitr4i 
 |-  ( <. z , w >. e. ( { <. x , y >. | ph } \ { <. x , y >. | ps } ) <-> <. z , w >. e. { <. x , y >. | ( ph /\ -. ps ) } )
20 3 4 19 eqrelriiv 
 |-  ( { <. x , y >. | ph } \ { <. x , y >. | ps } ) = { <. x , y >. | ( ph /\ -. ps ) }