bv-∃1

Theorem.

Arguments:

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

Dummy variables:

(sv),

Distinct variable conditions:

(, ), (, ), (, ),

Hypotheses:

( bound in )

Assertions:

( bound in )

Proof:

Hyp	Ref	Line	Expr
	Hypo	1	( bound in )
	ax10	2	(()((())(())))
2	aleqcom	3	(()((())(())))
	bv-∀b	4	( bound in (()))
4	df-Bvp	5	((())(()))
3, 5	rpi32	6	(()((())(())))
	bv-distvar	7	( bound in ())
	bv-distvar	8	( bound in ())
1	df-Bvp	9	()
9	ax1	10	(()())
	dveeq1	11	(()(()()))
8, 10, 11	fv-bid	12	(()((())(())))
7, 12	fv-alyd	13	(()((())(())))
6, 13	casei	14	((())(()))
14	df-Bvp	15	( bound in (()))
15	bv-∃	16	( bound in (()))
	df-∃1	17	((()))
16, 17	bvdef	18	( bound in )