Metamath Proof Explorer

Theorem inopab

Description: Intersection of two ordered pair class abstractions. (Contributed by NM, 30-Sep-2002)

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

Proof

Step Hyp Ref Expression
1 relopabv 
 |-  Rel { <. x , y >. | ph }
2 relin1 
 |-  ( Rel { <. x , y >. | ph } -> Rel ( { <. x , y >. | ph } i^i { <. x , y >. | ps } ) )
3 1 2 ax-mp 
 |-  Rel ( { <. x , y >. | ph } i^i { <. 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 vopelopabsb 
 |-  ( <. z , w >. e. { <. x , y >. | ps } <-> [ z / x ] [ w / y ] ps )
10 8 9 anbi12i 
 |-  ( ( <. z , w >. e. { <. x , y >. | ph } /\ <. z , w >. e. { <. x , y >. | ps } ) <-> ( [ z / x ] [ w / y ] ph /\ [ z / x ] [ w / y ] ps ) )
11 5 7 10 3bitr4ri 
 |-  ( ( <. z , w >. e. { <. x , y >. | ph } /\ <. z , w >. e. { <. x , y >. | ps } ) <-> [ z / x ] [ w / y ] ( ph /\ ps ) )
12 elin 
 |-  ( <. z , w >. e. ( { <. x , y >. | ph } i^i { <. x , y >. | ps } ) <-> ( <. z , w >. e. { <. x , y >. | ph } /\ <. z , w >. e. { <. x , y >. | ps } ) )
13 vopelopabsb 
 |-  ( <. z , w >. e. { <. x , y >. | ( ph /\ ps ) } <-> [ z / x ] [ w / y ] ( ph /\ ps ) )
14 11 12 13 3bitr4i 
 |-  ( <. z , w >. e. ( { <. x , y >. | ph } i^i { <. x , y >. | ps } ) <-> <. z , w >. e. { <. x , y >. | ( ph /\ ps ) } )
15 3 4 14 eqrelriiv 
 |-  ( { <. x , y >. | ph } i^i { <. x , y >. | ps } ) = { <. x , y >. | ( ph /\ ps ) }