Apply func_ext set (set → set) to the current goal.

Let x be given.

Apply func_ext set set to the current goal.

Let y be given.

We will prove pair x y = (x,y).

Apply tuple_pair to the current goal.

∎