Metamath Proof Explorer

Theorem opabid2

Description: A relation expressed as an ordered pair abstraction. (Contributed by NM, 11-Dec-2006)

Ref Expression
Assertion opabid2 
|- ( Rel A -> { <. x , y >. | <. x , y >. e. A } = A )

Proof

Step Hyp Ref Expression
1 vex 
 |-  z e. _V
2 vex 
 |-  w e. _V
3 opeq1 
 |-  ( x = z -> <. x , y >. = <. z , y >. )
4 3 eleq1d 
 |-  ( x = z -> ( <. x , y >. e. A <-> <. z , y >. e. A ) )
5 opeq2 
 |-  ( y = w -> <. z , y >. = <. z , w >. )
6 5 eleq1d 
 |-  ( y = w -> ( <. z , y >. e. A <-> <. z , w >. e. A ) )
7 1 2 4 6 opelopab 
 |-  ( <. z , w >. e. { <. x , y >. | <. x , y >. e. A } <-> <. z , w >. e. A )
8 7 gen2 
 |-  A. z A. w ( <. z , w >. e. { <. x , y >. | <. x , y >. e. A } <-> <. z , w >. e. A )
9 relopabv 
 |-  Rel { <. x , y >. | <. x , y >. e. A }
10 eqrel 
 |-  ( ( Rel { <. x , y >. | <. x , y >. e. A } /\ Rel A ) -> ( { <. x , y >. | <. x , y >. e. A } = A <-> A. z A. w ( <. z , w >. e. { <. x , y >. | <. x , y >. e. A } <-> <. z , w >. e. A ) ) )
11 9 10 mpan 
 |-  ( Rel A -> ( { <. x , y >. | <. x , y >. e. A } = A <-> A. z A. w ( <. z , w >. e. { <. x , y >. | <. x , y >. e. A } <-> <. z , w >. e. A ) ) )
12 8 11 mpbiri 
 |-  ( Rel A -> { <. x , y >. | <. x , y >. e. A } = A )