Step |
Hyp |
Ref |
Expression |
1 |
|
nfopab1 |
|- F/_ x { <. x , y >. | ph } |
2 |
|
nfopab1 |
|- F/_ x { <. x , y >. | ps } |
3 |
1 2
|
nfss |
|- F/ x { <. x , y >. | ph } C_ { <. x , y >. | ps } |
4 |
|
nfopab2 |
|- F/_ y { <. x , y >. | ph } |
5 |
|
nfopab2 |
|- F/_ y { <. x , y >. | ps } |
6 |
4 5
|
nfss |
|- F/ y { <. x , y >. | ph } C_ { <. x , y >. | ps } |
7 |
|
ssel |
|- ( { <. x , y >. | ph } C_ { <. x , y >. | ps } -> ( <. x , y >. e. { <. x , y >. | ph } -> <. x , y >. e. { <. x , y >. | ps } ) ) |
8 |
|
opabidw |
|- ( <. x , y >. e. { <. x , y >. | ph } <-> ph ) |
9 |
|
opabidw |
|- ( <. x , y >. e. { <. x , y >. | ps } <-> ps ) |
10 |
7 8 9
|
3imtr3g |
|- ( { <. x , y >. | ph } C_ { <. x , y >. | ps } -> ( ph -> ps ) ) |
11 |
6 10
|
alrimi |
|- ( { <. x , y >. | ph } C_ { <. x , y >. | ps } -> A. y ( ph -> ps ) ) |
12 |
3 11
|
alrimi |
|- ( { <. x , y >. | ph } C_ { <. x , y >. | ps } -> A. x A. y ( ph -> ps ) ) |
13 |
|
ssopab2 |
|- ( A. x A. y ( ph -> ps ) -> { <. x , y >. | ph } C_ { <. x , y >. | ps } ) |
14 |
12 13
|
impbii |
|- ( { <. x , y >. | ph } C_ { <. x , y >. | ps } <-> A. x A. y ( ph -> ps ) ) |