Step |
Hyp |
Ref |
Expression |
1 |
|
ssoprab2i.1 |
|- ( ph -> ps ) |
2 |
1
|
anim2i |
|- ( ( w = <. x , y >. /\ ph ) -> ( w = <. x , y >. /\ ps ) ) |
3 |
2
|
2eximi |
|- ( E. x E. y ( w = <. x , y >. /\ ph ) -> E. x E. y ( w = <. x , y >. /\ ps ) ) |
4 |
3
|
ssopab2i |
|- { <. w , z >. | E. x E. y ( w = <. x , y >. /\ ph ) } C_ { <. w , z >. | E. x E. y ( w = <. x , y >. /\ ps ) } |
5 |
|
dfoprab2 |
|- { <. <. x , y >. , z >. | ph } = { <. w , z >. | E. x E. y ( w = <. x , y >. /\ ph ) } |
6 |
|
dfoprab2 |
|- { <. <. x , y >. , z >. | ps } = { <. w , z >. | E. x E. y ( w = <. x , y >. /\ ps ) } |
7 |
4 5 6
|
3sstr4i |
|- { <. <. x , y >. , z >. | ph } C_ { <. <. x , y >. , z >. | ps } |