Step |
Hyp |
Ref |
Expression |
1 |
|
id |
|- ( ( ph -> ps ) -> ( ph -> ps ) ) |
2 |
1
|
anim2d |
|- ( ( ph -> ps ) -> ( ( w = <. <. x , y >. , z >. /\ ph ) -> ( w = <. <. x , y >. , z >. /\ ps ) ) ) |
3 |
2
|
aleximi |
|- ( A. z ( ph -> ps ) -> ( E. z ( w = <. <. x , y >. , z >. /\ ph ) -> E. z ( w = <. <. x , y >. , z >. /\ ps ) ) ) |
4 |
3
|
aleximi |
|- ( A. y A. z ( ph -> ps ) -> ( E. y E. z ( w = <. <. x , y >. , z >. /\ ph ) -> E. y E. z ( w = <. <. x , y >. , z >. /\ ps ) ) ) |
5 |
4
|
aleximi |
|- ( A. x A. y A. z ( ph -> ps ) -> ( E. x E. y E. z ( w = <. <. x , y >. , z >. /\ ph ) -> E. x E. y E. z ( w = <. <. x , y >. , z >. /\ ps ) ) ) |
6 |
5
|
ss2abdv |
|- ( A. x A. y A. z ( ph -> ps ) -> { w | E. x E. y E. z ( w = <. <. x , y >. , z >. /\ ph ) } C_ { w | E. x E. y E. z ( w = <. <. x , y >. , z >. /\ ps ) } ) |
7 |
|
df-oprab |
|- { <. <. x , y >. , z >. | ph } = { w | E. x E. y E. z ( w = <. <. x , y >. , z >. /\ ph ) } |
8 |
|
df-oprab |
|- { <. <. x , y >. , z >. | ps } = { w | E. x E. y E. z ( w = <. <. x , y >. , z >. /\ ps ) } |
9 |
6 7 8
|
3sstr4g |
|- ( A. x A. y A. z ( ph -> ps ) -> { <. <. x , y >. , z >. | ph } C_ { <. <. x , y >. , z >. | ps } ) |