eqsal

Theorem.

Arguments:

(sv), (st), (pr), (pr),

Distinct variable conditions:

(, ),

Hypotheses:

(()())

( bound in )

Assertions:

((()))

Proof:

Hyp	Ref	Line	Expr
	Hypo	1	(()())
		2	( bound in )
2	fv.eqal	3	()
1, 3	rpb33>>	4	(()())
4	im.bidi	5	((())(()))
5	eqt-∀-i	6	((())(()))
	ax1	7	((()))
7	ax5	8	((()))
2	df-Bvp	9	()
8, 9	syl	10	((()))
	ax9alt	11	((()))
10, 11	>bii	12	((()))
6, 12	><bitr	13	((()))