cbv-∃mo

Theorem.

Arguments:

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

Distinct variable conditions:

(, ),

Hypotheses:

(()())

( bound in )

( bound in )

Assertions:

()

Proof:

Hyp	Ref	Line	Expr
	Hypo	1	(()())
		2	( bound in )
		3	( bound in )
1, 2, 3	cbvex	4	()
1, 2, 3	cbv-∃1	5	()
4, 5	bi.bldim<>	6	(()())
	df-∃mo	7	(())
	df-∃mo	8	(())
6, 7, 8	<2bitr	9	()