Step |
Hyp |
Ref |
Expression |
1 |
|
cnvoprab.1 |
|- ( a = <. x , y >. -> ( ps <-> ph ) ) |
2 |
|
cnvoprab.2 |
|- ( ps -> a e. ( _V X. _V ) ) |
3 |
1
|
dfoprab3 |
|- { <. a , z >. | ( a e. ( _V X. _V ) /\ ps ) } = { <. <. x , y >. , z >. | ph } |
4 |
3
|
cnveqi |
|- `' { <. a , z >. | ( a e. ( _V X. _V ) /\ ps ) } = `' { <. <. x , y >. , z >. | ph } |
5 |
|
cnvopab |
|- `' { <. a , z >. | ( a e. ( _V X. _V ) /\ ps ) } = { <. z , a >. | ( a e. ( _V X. _V ) /\ ps ) } |
6 |
|
inopab |
|- ( { <. z , a >. | a e. ( _V X. _V ) } i^i { <. z , a >. | ps } ) = { <. z , a >. | ( a e. ( _V X. _V ) /\ ps ) } |
7 |
2
|
ssopab2i |
|- { <. z , a >. | ps } C_ { <. z , a >. | a e. ( _V X. _V ) } |
8 |
|
sseqin2 |
|- ( { <. z , a >. | ps } C_ { <. z , a >. | a e. ( _V X. _V ) } <-> ( { <. z , a >. | a e. ( _V X. _V ) } i^i { <. z , a >. | ps } ) = { <. z , a >. | ps } ) |
9 |
7 8
|
mpbi |
|- ( { <. z , a >. | a e. ( _V X. _V ) } i^i { <. z , a >. | ps } ) = { <. z , a >. | ps } |
10 |
5 6 9
|
3eqtr2i |
|- `' { <. a , z >. | ( a e. ( _V X. _V ) /\ ps ) } = { <. z , a >. | ps } |
11 |
4 10
|
eqtr3i |
|- `' { <. <. x , y >. , z >. | ph } = { <. z , a >. | ps } |