Step |
Hyp |
Ref |
Expression |
1 |
|
mosubopt |
|- ( A. x A. y E* z ph -> E* z E. x E. y ( w = <. x , y >. /\ ph ) ) |
2 |
1
|
alrimiv |
|- ( A. x A. y E* z ph -> A. w E* z E. x E. y ( w = <. x , y >. /\ ph ) ) |
3 |
|
dfoprab2 |
|- { <. <. x , y >. , z >. | ph } = { <. w , z >. | E. x E. y ( w = <. x , y >. /\ ph ) } |
4 |
3
|
funeqi |
|- ( Fun { <. <. x , y >. , z >. | ph } <-> Fun { <. w , z >. | E. x E. y ( w = <. x , y >. /\ ph ) } ) |
5 |
|
funopab |
|- ( Fun { <. w , z >. | E. x E. y ( w = <. x , y >. /\ ph ) } <-> A. w E* z E. x E. y ( w = <. x , y >. /\ ph ) ) |
6 |
4 5
|
bitr2i |
|- ( A. w E* z E. x E. y ( w = <. x , y >. /\ ph ) <-> Fun { <. <. x , y >. , z >. | ph } ) |
7 |
2 6
|
sylib |
|- ( A. x A. y E* z ph -> Fun { <. <. x , y >. , z >. | ph } ) |