ax4c

Theorem.

Arguments:

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

Hypotheses:

(()())

( bound in )

Assertions:

()

Proof:

Hyp	Ref	Line	Expr
	Hypo	1	(()())
		2	( bound in )
2	bv-¬	3	( bound in )
1	con	4	(()())
3, 4	ax4a	5	()
5	con>	6	()
	df-ex	7	()
6, 7	brpi22<	8	()