eqid

Theorem.

Arguments:

(st),

Dummy variables:

(sv),

Distinct variable conditions:

(, ),

Assertions:

()

Proof:

Hyp	Ref	Line	Expr
	ax9ex	1	()
	ax17	2	(()())
2	df-Bvp	3	( bound in ())
	ax8	4	(()(()()))
4	imabs	5	(()())
3, 5	imgen<i	6	(()())
1, 6	ax-mp	7	()