Define: f, a function mapping x to y

1	ALL(a):[ax => f(a)y]
	Premise

Define: finv, the inverse of f

2	ALL(a):[ax => finv(f(a))=a]
	Premise

	
	Suppose we have...

	3	px
		Premise

	Applying the definition of f...

	4	px => f(p)y
		U Spec, 1

	5	f(p)y
		Detach, 4, 3

	Applying the definition of finv...

	6	px => finv(f(p))=p
		U Spec, 2

	7	finv(f(p))=p
		Detach, 6, 3

	Joining lines 5 and 7...

	8	f(p)y & finv(f(p))=p
		Join, 5, 7

	As Required:

	9	EXIST(b):[by & finv(b)=p]
		E Gen, 8

10	px => EXIST(b):[by & finv(b)=p]
	Conclusion, 3

Generalizing...

11	ALL(a):[ax => EXIST(b):[by & finv(b)=a]]
	U Gen, 10