19.38

Theorem.

Arguments:

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

Assertions:

(()())

Proof:

Hyp	Ref	Line	Expr
	bv-∃b	1	( bound in )
	bv-∀b	2	( bound in )
1, 2	bv-→	3	( bound in ())
	spec-ex	4	()
	ax4	5	()
4, 5	syl34	6	(()())
3, 6	imgen>i	7	(()())