ax9ex

Theorem.

Arguments:

(sv), (st),

Distinct variable conditions:

(, ),

Assertions:

()

Proof:

Hyp	Ref	Line	Expr
	ax9	1	()
	df-ex	2	(()())
1, 2	bmp<	3	()