bv-sb-d1

Theorem.

Arguments:

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

Dummy variables:

(sv),

Distinct variable conditions:

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

Hypotheses:

( bound in )

Assertions:

( bound in [/])

Proof:

Hyp	Ref	Line	Expr
	Hypo	1	( bound in )
	ax10ex	2	(()((())(())))
	bv-idvar	3	( bound in ())
	bv-∃b	4	( bound in (()))
2, 3, 4	bvdefd	5	(()((())(())))
	ax16	6	(()(()()))
	ax12	7	(()(()(()())))
7	com12i	8	(()(()(()())))
6	ax1	9	(()(()(()())))
8, 9	casei	10	(()(()()))
10	naleqcoms	11	(()(()()))
	fv-nalx	12	( bound in ())
1	df-Bvp	13	()
13	ax1	14	(()())
11, 14	fv-and	15	(()((())(())))
12, 15	fv-exyd	16	(()((())(())))
5, 16	casei	17	((())(()))
17	df-Bvp	18	( bound in (()))
	ax17-bv	19	( bound in ())
18, 19	bv-∧	20	( bound in (()(())))
20	bv-∃	21	( bound in (()(())))
	df-sb	22	([/](()(())))
21, 22	bvdef	23	( bound in [/])