Theorem ac6s6

Description: Generalization of the Axiom of Choice to classes, moving the existence condition in the consequent. (Contributed by Giovanni Mascellani, 19-Aug-2018)

	Ref	Expression
Hypotheses	ac6s6.1	$$⊢Ⅎy\psi$$
	ac6s6.2	$$⊢A\in \mathrm{V}$$
	ac6s6.3	$$⊢y=f\left(x\right)\to \left(\phi \leftrightarrow \psi \right)$$
Assertion	ac6s6	$$⊢\exists f\forall x\in A\left(\exists y\phi \to \psi \right)$$

Proof

Step	Hyp	Ref	Expression
1		ac6s6.1	$$⊢Ⅎy\psi$$
2		ac6s6.2	$$⊢A\in \mathrm{V}$$
3		ac6s6.3	$$⊢y=f\left(x\right)\to \left(\phi \leftrightarrow \psi \right)$$
4		hbe1	$$⊢\exists y\phi \to \forall y\exists y\phi$$
5		iftrue	$$⊢\exists y\phi \to if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)=\left\{y|\phi \right\}$$
6	5	eqabrd	$$⊢\exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \phi \right)$$
7	4 6	exbidh	$$⊢\exists y\phi \to \left(\exists yy\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \exists y\phi \right)$$
8	7	ibir	$$⊢\exists y\phi \to \exists yy\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)$$
9		vex	$$⊢y\in \mathrm{V}$$
10	9	exgen	$$⊢\exists yy\in \mathrm{V}$$
11	4	hbn	$$⊢\neg \exists y\phi \to \forall y\neg \exists y\phi$$
12		iffalse	$$⊢\neg \exists y\phi \to if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)=\mathrm{V}$$
13	12	eleq2d	$$⊢\neg \exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow y\in \mathrm{V}\right)$$
14	11 13	exbidh	$$⊢\neg \exists y\phi \to \left(\exists yy\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \exists yy\in \mathrm{V}\right)$$
15	10 14	mpbiri	$$⊢\neg \exists y\phi \to \exists yy\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)$$
16	8 15	pm2.61i	$$⊢\exists yy\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)$$
17	16	rgenw	$$⊢\forall x\in A\exists yy\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)$$
18		nfe1	$$⊢Ⅎy\exists y\phi$$
19	18 1	nfim	$$⊢Ⅎy\left(\exists y\phi \to \psi \right)$$
20		id	$$⊢\neg \phi \to \neg \phi$$
21	20	a1i	$$⊢\neg \left(\left(y=f\left(x\right)\to \left(\phi \leftrightarrow \psi \right)\right)\to \left(\left(\exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \phi \right)\right)\to \left(\exists y\phi \to \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)\right)\right)\to \left(\neg \phi \to \neg \phi \right)$$
22		ax-1	$$⊢\neg \left(\left(y=f\left(x\right)\to \left(\phi \leftrightarrow \psi \right)\right)\to \left(\left(\exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \phi \right)\right)\to \left(\exists y\phi \to \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)\right)\right)\to \left(\neg \phi \to \neg \left(\left(y=f\left(x\right)\to \left(\phi \leftrightarrow \psi \right)\right)\to \left(\left(\exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \phi \right)\right)\to \left(\exists y\phi \to \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)\right)\right)\right)$$
23		tsim3	$$⊢\neg \left(\left(y=f\left(x\right)\to \left(\phi \leftrightarrow \psi \right)\right)\to \left(\left(\exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \phi \right)\right)\to \left(\exists y\phi \to \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)\right)\right)\to \left(\neg \left(\left(\exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \phi \right)\right)\to \left(\exists y\phi \to \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)\right)\vee \left(\left(y=f\left(x\right)\to \left(\phi \leftrightarrow \psi \right)\right)\to \left(\left(\exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \phi \right)\right)\to \left(\exists y\phi \to \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)\right)\right)\right)$$
24	23	a1d	$$⊢\neg \left(\left(y=f\left(x\right)\to \left(\phi \leftrightarrow \psi \right)\right)\to \left(\left(\exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \phi \right)\right)\to \left(\exists y\phi \to \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)\right)\right)\to \left(\neg \phi \to \left(\neg \left(\left(\exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \phi \right)\right)\to \left(\exists y\phi \to \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)\right)\vee \left(\left(y=f\left(x\right)\to \left(\phi \leftrightarrow \psi \right)\right)\to \left(\left(\exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \phi \right)\right)\to \left(\exists y\phi \to \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)\right)\right)\right)\right)$$
25	22 24	cnf2dd	$$⊢\neg \left(\left(y=f\left(x\right)\to \left(\phi \leftrightarrow \psi \right)\right)\to \left(\left(\exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \phi \right)\right)\to \left(\exists y\phi \to \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)\right)\right)\to \left(\neg \phi \to \neg \left(\left(\exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \phi \right)\right)\to \left(\exists y\phi \to \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)\right)\right)$$
26		tsim3	$$⊢\neg \left(\left(y=f\left(x\right)\to \left(\phi \leftrightarrow \psi \right)\right)\to \left(\left(\exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \phi \right)\right)\to \left(\exists y\phi \to \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)\right)\right)\to \left(\neg \left(\exists y\phi \to \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)\vee \left(\left(\exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \phi \right)\right)\to \left(\exists y\phi \to \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)\right)\right)$$
27	26	a1d	$$⊢\neg \left(\left(y=f\left(x\right)\to \left(\phi \leftrightarrow \psi \right)\right)\to \left(\left(\exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \phi \right)\right)\to \left(\exists y\phi \to \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)\right)\right)\to \left(\neg \phi \to \left(\neg \left(\exists y\phi \to \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)\vee \left(\left(\exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \phi \right)\right)\to \left(\exists y\phi \to \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)\right)\right)\right)$$
28	25 27	cnf2dd	$$⊢\neg \left(\left(y=f\left(x\right)\to \left(\phi \leftrightarrow \psi \right)\right)\to \left(\left(\exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \phi \right)\right)\to \left(\exists y\phi \to \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)\right)\right)\to \left(\neg \phi \to \neg \left(\exists y\phi \to \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)\right)$$
29		tsim2	$$⊢\neg \left(\left(y=f\left(x\right)\to \left(\phi \leftrightarrow \psi \right)\right)\to \left(\left(\exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \phi \right)\right)\to \left(\exists y\phi \to \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)\right)\right)\to \left(\exists y\phi \vee \left(\exists y\phi \to \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)\right)$$
30	29	a1d	$$⊢\neg \left(\left(y=f\left(x\right)\to \left(\phi \leftrightarrow \psi \right)\right)\to \left(\left(\exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \phi \right)\right)\to \left(\exists y\phi \to \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)\right)\right)\to \left(\neg \phi \to \left(\exists y\phi \vee \left(\exists y\phi \to \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)\right)\right)$$
31	28 30	cnf2dd	$$⊢\neg \left(\left(y=f\left(x\right)\to \left(\phi \leftrightarrow \psi \right)\right)\to \left(\left(\exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \phi \right)\right)\to \left(\exists y\phi \to \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)\right)\right)\to \left(\neg \phi \to \exists y\phi \right)$$
32		tsim2	$$⊢\neg \left(\left(y=f\left(x\right)\to \left(\phi \leftrightarrow \psi \right)\right)\to \left(\left(\exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \phi \right)\right)\to \left(\exists y\phi \to \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)\right)\right)\to \left(\left(\exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \phi \right)\right)\vee \left(\left(\exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \phi \right)\right)\to \left(\exists y\phi \to \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)\right)\right)$$
33	32	a1d	$$⊢\neg \left(\left(y=f\left(x\right)\to \left(\phi \leftrightarrow \psi \right)\right)\to \left(\left(\exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \phi \right)\right)\to \left(\exists y\phi \to \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)\right)\right)\to \left(\neg \phi \to \left(\left(\exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \phi \right)\right)\vee \left(\left(\exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \phi \right)\right)\to \left(\exists y\phi \to \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)\right)\right)\right)$$
34	25 33	cnf2dd	$$⊢\neg \left(\left(y=f\left(x\right)\to \left(\phi \leftrightarrow \psi \right)\right)\to \left(\left(\exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \phi \right)\right)\to \left(\exists y\phi \to \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)\right)\right)\to \left(\neg \phi \to \left(\exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \phi \right)\right)\right)$$
35	31 34	mpdd	$$⊢\neg \left(\left(y=f\left(x\right)\to \left(\phi \leftrightarrow \psi \right)\right)\to \left(\left(\exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \phi \right)\right)\to \left(\exists y\phi \to \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)\right)\right)\to \left(\neg \phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \phi \right)\right)$$
36		tsbi4	$$⊢\neg \left(\left(y=f\left(x\right)\to \left(\phi \leftrightarrow \psi \right)\right)\to \left(\left(\exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \phi \right)\right)\to \left(\exists y\phi \to \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)\right)\right)\to \left(\left(\neg y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\vee \phi \right)\vee \neg \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \phi \right)\right)$$
37	36	a1d	$$⊢\neg \left(\left(y=f\left(x\right)\to \left(\phi \leftrightarrow \psi \right)\right)\to \left(\left(\exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \phi \right)\right)\to \left(\exists y\phi \to \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)\right)\right)\to \left(\neg \phi \to \left(\left(\neg y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\vee \phi \right)\vee \neg \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \phi \right)\right)\right)$$
38	35 37	cnfn2dd	$$⊢\neg \left(\left(y=f\left(x\right)\to \left(\phi \leftrightarrow \psi \right)\right)\to \left(\left(\exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \phi \right)\right)\to \left(\exists y\phi \to \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)\right)\right)\to \left(\neg \phi \to \left(\neg y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\vee \phi \right)\right)$$
39	21 38	cnf2dd	$$⊢\neg \left(\left(y=f\left(x\right)\to \left(\phi \leftrightarrow \psi \right)\right)\to \left(\left(\exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \phi \right)\right)\to \left(\exists y\phi \to \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)\right)\right)\to \left(\neg \phi \to \neg y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\right)$$
40		tsim3	$$⊢\neg \left(\left(y=f\left(x\right)\to \left(\phi \leftrightarrow \psi \right)\right)\to \left(\left(\exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \phi \right)\right)\to \left(\exists y\phi \to \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)\right)\right)\to \left(\neg \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\vee \left(\exists y\phi \to \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)\right)$$
41	40	a1d	$$⊢\neg \left(\left(y=f\left(x\right)\to \left(\phi \leftrightarrow \psi \right)\right)\to \left(\left(\exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \phi \right)\right)\to \left(\exists y\phi \to \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)\right)\right)\to \left(\neg \phi \to \left(\neg \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\vee \left(\exists y\phi \to \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)\right)\right)$$
42	28 41	cnf2dd	$$⊢\neg \left(\left(y=f\left(x\right)\to \left(\phi \leftrightarrow \psi \right)\right)\to \left(\left(\exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \phi \right)\right)\to \left(\exists y\phi \to \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)\right)\right)\to \left(\neg \phi \to \neg \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)$$
43		tsim3	$$⊢\neg \left(\left(y=f\left(x\right)\to \left(\phi \leftrightarrow \psi \right)\right)\to \left(\left(\exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \phi \right)\right)\to \left(\exists y\phi \to \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)\right)\right)\to \left(\neg \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\vee \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)$$
44	43	a1d	$$⊢\neg \left(\left(y=f\left(x\right)\to \left(\phi \leftrightarrow \psi \right)\right)\to \left(\left(\exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \phi \right)\right)\to \left(\exists y\phi \to \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)\right)\right)\to \left(\neg \phi \to \left(\neg \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\vee \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)\right)$$
45	42 44	cnf2dd	$$⊢\neg \left(\left(y=f\left(x\right)\to \left(\phi \leftrightarrow \psi \right)\right)\to \left(\left(\exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \phi \right)\right)\to \left(\exists y\phi \to \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)\right)\right)\to \left(\neg \phi \to \neg \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)$$
46		tsbi2	$$⊢\neg \left(\left(y=f\left(x\right)\to \left(\phi \leftrightarrow \psi \right)\right)\to \left(\left(\exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \phi \right)\right)\to \left(\exists y\phi \to \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)\right)\right)\to \left(\left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\vee \left(\exists y\phi \to \psi \right)\right)\vee \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)$$
47	46	a1d	$$⊢\neg \left(\left(y=f\left(x\right)\to \left(\phi \leftrightarrow \psi \right)\right)\to \left(\left(\exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \phi \right)\right)\to \left(\exists y\phi \to \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)\right)\right)\to \left(\neg \phi \to \left(\left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\vee \left(\exists y\phi \to \psi \right)\right)\vee \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)$$
48	45 47	cnf2dd	$$⊢\neg \left(\left(y=f\left(x\right)\to \left(\phi \leftrightarrow \psi \right)\right)\to \left(\left(\exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \phi \right)\right)\to \left(\exists y\phi \to \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)\right)\right)\to \left(\neg \phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\vee \left(\exists y\phi \to \psi \right)\right)\right)$$
49	39 48	cnf1dd	$$⊢\neg \left(\left(y=f\left(x\right)\to \left(\phi \leftrightarrow \psi \right)\right)\to \left(\left(\exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \phi \right)\right)\to \left(\exists y\phi \to \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)\right)\right)\to \left(\neg \phi \to \left(\exists y\phi \to \psi \right)\right)$$
50		tsim2	$$⊢\neg \left(\left(y=f\left(x\right)\to \left(\phi \leftrightarrow \psi \right)\right)\to \left(\left(\exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \phi \right)\right)\to \left(\exists y\phi \to \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)\right)\right)\to \left(y=f\left(x\right)\vee \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)$$
51	50	a1d	$$⊢\neg \left(\left(y=f\left(x\right)\to \left(\phi \leftrightarrow \psi \right)\right)\to \left(\left(\exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \phi \right)\right)\to \left(\exists y\phi \to \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)\right)\right)\to \left(\neg \phi \to \left(y=f\left(x\right)\vee \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)\right)$$
52	42 51	cnf2dd	$$⊢\neg \left(\left(y=f\left(x\right)\to \left(\phi \leftrightarrow \psi \right)\right)\to \left(\left(\exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \phi \right)\right)\to \left(\exists y\phi \to \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)\right)\right)\to \left(\neg \phi \to y=f\left(x\right)\right)$$
53		simplim	$$⊢\neg \left(\left(y=f\left(x\right)\to \left(\phi \leftrightarrow \psi \right)\right)\to \left(\left(\exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \phi \right)\right)\to \left(\exists y\phi \to \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)\right)\right)\to \left(y=f\left(x\right)\to \left(\phi \leftrightarrow \psi \right)\right)$$
54	52 53	syld	$$⊢\neg \left(\left(y=f\left(x\right)\to \left(\phi \leftrightarrow \psi \right)\right)\to \left(\left(\exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \phi \right)\right)\to \left(\exists y\phi \to \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)\right)\right)\to \left(\neg \phi \to \left(\phi \leftrightarrow \psi \right)\right)$$
55		tsbi3	$$⊢\neg \left(\left(y=f\left(x\right)\to \left(\phi \leftrightarrow \psi \right)\right)\to \left(\left(\exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \phi \right)\right)\to \left(\exists y\phi \to \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)\right)\right)\to \left(\left(\phi \vee \neg \psi \right)\vee \neg \left(\phi \leftrightarrow \psi \right)\right)$$
56	55	a1d	$$⊢\neg \left(\left(y=f\left(x\right)\to \left(\phi \leftrightarrow \psi \right)\right)\to \left(\left(\exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \phi \right)\right)\to \left(\exists y\phi \to \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)\right)\right)\to \left(\neg \phi \to \left(\left(\phi \vee \neg \psi \right)\vee \neg \left(\phi \leftrightarrow \psi \right)\right)\right)$$
57	54 56	cnfn2dd	$$⊢\neg \left(\left(y=f\left(x\right)\to \left(\phi \leftrightarrow \psi \right)\right)\to \left(\left(\exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \phi \right)\right)\to \left(\exists y\phi \to \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)\right)\right)\to \left(\neg \phi \to \left(\phi \vee \neg \psi \right)\right)$$
58	21 57	cnf1dd	$$⊢\neg \left(\left(y=f\left(x\right)\to \left(\phi \leftrightarrow \psi \right)\right)\to \left(\left(\exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \phi \right)\right)\to \left(\exists y\phi \to \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)\right)\right)\to \left(\neg \phi \to \neg \psi \right)$$
59		tsim1	$$⊢\neg \left(\left(y=f\left(x\right)\to \left(\phi \leftrightarrow \psi \right)\right)\to \left(\left(\exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \phi \right)\right)\to \left(\exists y\phi \to \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)\right)\right)\to \left(\left(\neg \exists y\phi \vee \psi \right)\vee \neg \left(\exists y\phi \to \psi \right)\right)$$
60	59	a1d	$$⊢\neg \left(\left(y=f\left(x\right)\to \left(\phi \leftrightarrow \psi \right)\right)\to \left(\left(\exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \phi \right)\right)\to \left(\exists y\phi \to \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)\right)\right)\to \left(\neg \phi \to \left(\left(\neg \exists y\phi \vee \psi \right)\vee \neg \left(\exists y\phi \to \psi \right)\right)\right)$$
61	60	or32dd	$$⊢\neg \left(\left(y=f\left(x\right)\to \left(\phi \leftrightarrow \psi \right)\right)\to \left(\left(\exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \phi \right)\right)\to \left(\exists y\phi \to \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)\right)\right)\to \left(\neg \phi \to \left(\left(\neg \exists y\phi \vee \neg \left(\exists y\phi \to \psi \right)\right)\vee \psi \right)\right)$$
62	58 61	cnf2dd	$$⊢\neg \left(\left(y=f\left(x\right)\to \left(\phi \leftrightarrow \psi \right)\right)\to \left(\left(\exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \phi \right)\right)\to \left(\exists y\phi \to \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)\right)\right)\to \left(\neg \phi \to \left(\neg \exists y\phi \vee \neg \left(\exists y\phi \to \psi \right)\right)\right)$$
63	31 62	cnfn1dd	$$⊢\neg \left(\left(y=f\left(x\right)\to \left(\phi \leftrightarrow \psi \right)\right)\to \left(\left(\exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \phi \right)\right)\to \left(\exists y\phi \to \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)\right)\right)\to \left(\neg \phi \to \neg \left(\exists y\phi \to \psi \right)\right)$$
64	49 63	contrd	$$⊢\neg \left(\left(y=f\left(x\right)\to \left(\phi \leftrightarrow \psi \right)\right)\to \left(\left(\exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \phi \right)\right)\to \left(\exists y\phi \to \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)\right)\right)\to \phi$$
65	64	a1d	$$⊢\neg \left(\left(y=f\left(x\right)\to \left(\phi \leftrightarrow \psi \right)\right)\to \left(\left(\exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \phi \right)\right)\to \left(\exists y\phi \to \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)\right)\right)\to \left(\neg \perp \to \phi \right)$$
66		ax-1	$$⊢\neg \left(\left(y=f\left(x\right)\to \left(\phi \leftrightarrow \psi \right)\right)\to \left(\left(\exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \phi \right)\right)\to \left(\exists y\phi \to \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)\right)\right)\to \left(\neg \perp \to \neg \left(\left(y=f\left(x\right)\to \left(\phi \leftrightarrow \psi \right)\right)\to \left(\left(\exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \phi \right)\right)\to \left(\exists y\phi \to \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)\right)\right)\right)$$
67	23	a1d	$$⊢\neg \left(\left(y=f\left(x\right)\to \left(\phi \leftrightarrow \psi \right)\right)\to \left(\left(\exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \phi \right)\right)\to \left(\exists y\phi \to \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)\right)\right)\to \left(\neg \perp \to \left(\neg \left(\left(\exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \phi \right)\right)\to \left(\exists y\phi \to \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)\right)\vee \left(\left(y=f\left(x\right)\to \left(\phi \leftrightarrow \psi \right)\right)\to \left(\left(\exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \phi \right)\right)\to \left(\exists y\phi \to \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)\right)\right)\right)\right)$$
68	66 67	cnf2dd	$$⊢\neg \left(\left(y=f\left(x\right)\to \left(\phi \leftrightarrow \psi \right)\right)\to \left(\left(\exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \phi \right)\right)\to \left(\exists y\phi \to \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)\right)\right)\to \left(\neg \perp \to \neg \left(\left(\exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \phi \right)\right)\to \left(\exists y\phi \to \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)\right)\right)$$
69	26	a1d	$$⊢\neg \left(\left(y=f\left(x\right)\to \left(\phi \leftrightarrow \psi \right)\right)\to \left(\left(\exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \phi \right)\right)\to \left(\exists y\phi \to \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)\right)\right)\to \left(\neg \perp \to \left(\neg \left(\exists y\phi \to \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)\vee \left(\left(\exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \phi \right)\right)\to \left(\exists y\phi \to \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)\right)\right)\right)$$
70	68 69	cnf2dd	$$⊢\neg \left(\left(y=f\left(x\right)\to \left(\phi \leftrightarrow \psi \right)\right)\to \left(\left(\exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \phi \right)\right)\to \left(\exists y\phi \to \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)\right)\right)\to \left(\neg \perp \to \neg \left(\exists y\phi \to \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)\right)$$
71	29	a1d	$$⊢\neg \left(\left(y=f\left(x\right)\to \left(\phi \leftrightarrow \psi \right)\right)\to \left(\left(\exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \phi \right)\right)\to \left(\exists y\phi \to \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)\right)\right)\to \left(\neg \perp \to \left(\exists y\phi \vee \left(\exists y\phi \to \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)\right)\right)$$
72	70 71	cnf2dd	$$⊢\neg \left(\left(y=f\left(x\right)\to \left(\phi \leftrightarrow \psi \right)\right)\to \left(\left(\exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \phi \right)\right)\to \left(\exists y\phi \to \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)\right)\right)\to \left(\neg \perp \to \exists y\phi \right)$$
73	32	a1d	$$⊢\neg \left(\left(y=f\left(x\right)\to \left(\phi \leftrightarrow \psi \right)\right)\to \left(\left(\exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \phi \right)\right)\to \left(\exists y\phi \to \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)\right)\right)\to \left(\neg \perp \to \left(\left(\exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \phi \right)\right)\vee \left(\left(\exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \phi \right)\right)\to \left(\exists y\phi \to \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)\right)\right)\right)$$
74	68 73	cnf2dd	$$⊢\neg \left(\left(y=f\left(x\right)\to \left(\phi \leftrightarrow \psi \right)\right)\to \left(\left(\exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \phi \right)\right)\to \left(\exists y\phi \to \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)\right)\right)\to \left(\neg \perp \to \left(\exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \phi \right)\right)\right)$$
75	72 74	mpdd	$$⊢\neg \left(\left(y=f\left(x\right)\to \left(\phi \leftrightarrow \psi \right)\right)\to \left(\left(\exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \phi \right)\right)\to \left(\exists y\phi \to \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)\right)\right)\to \left(\neg \perp \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \phi \right)\right)$$
76		tsbi3	$$⊢\neg \left(\left(y=f\left(x\right)\to \left(\phi \leftrightarrow \psi \right)\right)\to \left(\left(\exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \phi \right)\right)\to \left(\exists y\phi \to \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)\right)\right)\to \left(\left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\vee \neg \phi \right)\vee \neg \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \phi \right)\right)$$
77	76	a1d	$$⊢\neg \left(\left(y=f\left(x\right)\to \left(\phi \leftrightarrow \psi \right)\right)\to \left(\left(\exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \phi \right)\right)\to \left(\exists y\phi \to \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)\right)\right)\to \left(\neg \perp \to \left(\left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\vee \neg \phi \right)\vee \neg \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \phi \right)\right)\right)$$
78	75 77	cnfn2dd	$$⊢\neg \left(\left(y=f\left(x\right)\to \left(\phi \leftrightarrow \psi \right)\right)\to \left(\left(\exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \phi \right)\right)\to \left(\exists y\phi \to \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)\right)\right)\to \left(\neg \perp \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\vee \neg \phi \right)\right)$$
79	65 78	cnfn2dd	$$⊢\neg \left(\left(y=f\left(x\right)\to \left(\phi \leftrightarrow \psi \right)\right)\to \left(\left(\exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \phi \right)\right)\to \left(\exists y\phi \to \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)\right)\right)\to \left(\neg \perp \to y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\right)$$
80	40	a1d	$$⊢\neg \left(\left(y=f\left(x\right)\to \left(\phi \leftrightarrow \psi \right)\right)\to \left(\left(\exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \phi \right)\right)\to \left(\exists y\phi \to \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)\right)\right)\to \left(\neg \perp \to \left(\neg \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\vee \left(\exists y\phi \to \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)\right)\right)$$
81	70 80	cnf2dd	$$⊢\neg \left(\left(y=f\left(x\right)\to \left(\phi \leftrightarrow \psi \right)\right)\to \left(\left(\exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \phi \right)\right)\to \left(\exists y\phi \to \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)\right)\right)\to \left(\neg \perp \to \neg \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)$$
82	50	a1d	$$⊢\neg \left(\left(y=f\left(x\right)\to \left(\phi \leftrightarrow \psi \right)\right)\to \left(\left(\exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \phi \right)\right)\to \left(\exists y\phi \to \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)\right)\right)\to \left(\neg \perp \to \left(y=f\left(x\right)\vee \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)\right)$$
83	81 82	cnf2dd	$$⊢\neg \left(\left(y=f\left(x\right)\to \left(\phi \leftrightarrow \psi \right)\right)\to \left(\left(\exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \phi \right)\right)\to \left(\exists y\phi \to \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)\right)\right)\to \left(\neg \perp \to y=f\left(x\right)\right)$$
84	83 53	syld	$$⊢\neg \left(\left(y=f\left(x\right)\to \left(\phi \leftrightarrow \psi \right)\right)\to \left(\left(\exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \phi \right)\right)\to \left(\exists y\phi \to \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)\right)\right)\to \left(\neg \perp \to \left(\phi \leftrightarrow \psi \right)\right)$$
85		tsbi4	$$⊢\neg \left(\left(y=f\left(x\right)\to \left(\phi \leftrightarrow \psi \right)\right)\to \left(\left(\exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \phi \right)\right)\to \left(\exists y\phi \to \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)\right)\right)\to \left(\left(\neg \phi \vee \psi \right)\vee \neg \left(\phi \leftrightarrow \psi \right)\right)$$
86	85	a1d	$$⊢\neg \left(\left(y=f\left(x\right)\to \left(\phi \leftrightarrow \psi \right)\right)\to \left(\left(\exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \phi \right)\right)\to \left(\exists y\phi \to \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)\right)\right)\to \left(\neg \perp \to \left(\left(\neg \phi \vee \psi \right)\vee \neg \left(\phi \leftrightarrow \psi \right)\right)\right)$$
87	84 86	cnfn2dd	$$⊢\neg \left(\left(y=f\left(x\right)\to \left(\phi \leftrightarrow \psi \right)\right)\to \left(\left(\exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \phi \right)\right)\to \left(\exists y\phi \to \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)\right)\right)\to \left(\neg \perp \to \left(\neg \phi \vee \psi \right)\right)$$
88	65 87	cnfn1dd	$$⊢\neg \left(\left(y=f\left(x\right)\to \left(\phi \leftrightarrow \psi \right)\right)\to \left(\left(\exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \phi \right)\right)\to \left(\exists y\phi \to \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)\right)\right)\to \left(\neg \perp \to \psi \right)$$
89	88	a1dd	$$⊢\neg \left(\left(y=f\left(x\right)\to \left(\phi \leftrightarrow \psi \right)\right)\to \left(\left(\exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \phi \right)\right)\to \left(\exists y\phi \to \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)\right)\right)\to \left(\neg \perp \to \left(\exists y\phi \to \psi \right)\right)$$
90		tsbi1	$$⊢\neg \left(\left(y=f\left(x\right)\to \left(\phi \leftrightarrow \psi \right)\right)\to \left(\left(\exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \phi \right)\right)\to \left(\exists y\phi \to \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)\right)\right)\to \left(\left(\neg y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\vee \neg \left(\exists y\phi \to \psi \right)\right)\vee \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)$$
91	90	a1d	$$⊢\neg \left(\left(y=f\left(x\right)\to \left(\phi \leftrightarrow \psi \right)\right)\to \left(\left(\exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \phi \right)\right)\to \left(\exists y\phi \to \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)\right)\right)\to \left(\neg \perp \to \left(\left(\neg y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\vee \neg \left(\exists y\phi \to \psi \right)\right)\vee \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)$$
92	91	or32dd	$$⊢\neg \left(\left(y=f\left(x\right)\to \left(\phi \leftrightarrow \psi \right)\right)\to \left(\left(\exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \phi \right)\right)\to \left(\exists y\phi \to \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)\right)\right)\to \left(\neg \perp \to \left(\left(\neg y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\vee \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\vee \neg \left(\exists y\phi \to \psi \right)\right)\right)$$
93	89 92	cnfn2dd	$$⊢\neg \left(\left(y=f\left(x\right)\to \left(\phi \leftrightarrow \psi \right)\right)\to \left(\left(\exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \phi \right)\right)\to \left(\exists y\phi \to \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)\right)\right)\to \left(\neg \perp \to \left(\neg y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\vee \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)$$
94	79 93	cnfn1dd	$$⊢\neg \left(\left(y=f\left(x\right)\to \left(\phi \leftrightarrow \psi \right)\right)\to \left(\left(\exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \phi \right)\right)\to \left(\exists y\phi \to \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)\right)\right)\to \left(\neg \perp \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)$$
95	43	a1d	$$⊢\neg \left(\left(y=f\left(x\right)\to \left(\phi \leftrightarrow \psi \right)\right)\to \left(\left(\exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \phi \right)\right)\to \left(\exists y\phi \to \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)\right)\right)\to \left(\neg \perp \to \left(\neg \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\vee \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)\right)$$
96	81 95	cnf2dd	$$⊢\neg \left(\left(y=f\left(x\right)\to \left(\phi \leftrightarrow \psi \right)\right)\to \left(\left(\exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \phi \right)\right)\to \left(\exists y\phi \to \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)\right)\right)\to \left(\neg \perp \to \neg \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)$$
97	94 96	contrd	$$⊢\neg \left(\left(y=f\left(x\right)\to \left(\phi \leftrightarrow \psi \right)\right)\to \left(\left(\exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \phi \right)\right)\to \left(\exists y\phi \to \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)\right)\right)\to \perp$$
98	97	efald2	$$⊢\left(y=f\left(x\right)\to \left(\phi \leftrightarrow \psi \right)\right)\to \left(\left(\exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \phi \right)\right)\to \left(\exists y\phi \to \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)\right)$$
99	3 98	ax-mp	$$⊢\left(\exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \phi \right)\right)\to \left(\exists y\phi \to \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)$$
100	6 99	ax-mp	$$⊢\exists y\phi \to \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)$$
101	9	a1i	$$⊢\neg \exists y\phi \to y\in \mathrm{V}$$
102		id	$$⊢\neg \left(\left(\neg \exists y\phi \to y\in \mathrm{V}\right)\to \left(\left(\neg \exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow y\in \mathrm{V}\right)\right)\to \left(\neg \exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \top \right)\right)\right)\right)\to \neg \left(\left(\neg \exists y\phi \to y\in \mathrm{V}\right)\to \left(\left(\neg \exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow y\in \mathrm{V}\right)\right)\to \left(\neg \exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \top \right)\right)\right)\right)$$
103		tsim2	$$⊢\neg \left(\left(\neg \exists y\phi \to y\in \mathrm{V}\right)\to \left(\left(\neg \exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow y\in \mathrm{V}\right)\right)\to \left(\neg \exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \top \right)\right)\right)\right)\to \left(\neg \exists y\phi \vee \left(\neg \exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \top \right)\right)\right)$$
104	103	ord	$$⊢\neg \left(\left(\neg \exists y\phi \to y\in \mathrm{V}\right)\to \left(\left(\neg \exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow y\in \mathrm{V}\right)\right)\to \left(\neg \exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \top \right)\right)\right)\right)\to \left(\neg \neg \exists y\phi \to \left(\neg \exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \top \right)\right)\right)$$
105	104	a1dd	$$⊢\neg \left(\left(\neg \exists y\phi \to y\in \mathrm{V}\right)\to \left(\left(\neg \exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow y\in \mathrm{V}\right)\right)\to \left(\neg \exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \top \right)\right)\right)\right)\to \left(\neg \neg \exists y\phi \to \left(\left(\neg \exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow y\in \mathrm{V}\right)\right)\to \left(\neg \exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \top \right)\right)\right)\right)$$
106	105	a1dd	$$⊢\neg \left(\left(\neg \exists y\phi \to y\in \mathrm{V}\right)\to \left(\left(\neg \exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow y\in \mathrm{V}\right)\right)\to \left(\neg \exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \top \right)\right)\right)\right)\to \left(\neg \neg \exists y\phi \to \left(\left(\neg \exists y\phi \to y\in \mathrm{V}\right)\to \left(\left(\neg \exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow y\in \mathrm{V}\right)\right)\to \left(\neg \exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \top \right)\right)\right)\right)\right)$$
107	102 106	mt3d	$$⊢\neg \left(\left(\neg \exists y\phi \to y\in \mathrm{V}\right)\to \left(\left(\neg \exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow y\in \mathrm{V}\right)\right)\to \left(\neg \exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \top \right)\right)\right)\right)\to \neg \exists y\phi$$
108	107	a1d	$$⊢\neg \left(\left(\neg \exists y\phi \to y\in \mathrm{V}\right)\to \left(\left(\neg \exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow y\in \mathrm{V}\right)\right)\to \left(\neg \exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \top \right)\right)\right)\right)\to \left(\neg \perp \to \neg \exists y\phi \right)$$
109		simplim	$$⊢\neg \left(\left(\neg \exists y\phi \to y\in \mathrm{V}\right)\to \left(\left(\neg \exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow y\in \mathrm{V}\right)\right)\to \left(\neg \exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \top \right)\right)\right)\right)\to \left(\neg \exists y\phi \to y\in \mathrm{V}\right)$$
110	108 109	syld	$$⊢\neg \left(\left(\neg \exists y\phi \to y\in \mathrm{V}\right)\to \left(\left(\neg \exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow y\in \mathrm{V}\right)\right)\to \left(\neg \exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \top \right)\right)\right)\right)\to \left(\neg \perp \to y\in \mathrm{V}\right)$$
111		tsim2	$$⊢\neg \left(\left(\neg \exists y\phi \to y\in \mathrm{V}\right)\to \left(\left(\neg \exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow y\in \mathrm{V}\right)\right)\to \left(\neg \exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \top \right)\right)\right)\right)\to \left(\left(\neg \exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow y\in \mathrm{V}\right)\right)\vee \left(\left(\neg \exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow y\in \mathrm{V}\right)\right)\to \left(\neg \exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \top \right)\right)\right)\right)$$
112	111	ord	$$⊢\neg \left(\left(\neg \exists y\phi \to y\in \mathrm{V}\right)\to \left(\left(\neg \exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow y\in \mathrm{V}\right)\right)\to \left(\neg \exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \top \right)\right)\right)\right)\to \left(\neg \left(\neg \exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow y\in \mathrm{V}\right)\right)\to \left(\left(\neg \exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow y\in \mathrm{V}\right)\right)\to \left(\neg \exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \top \right)\right)\right)\right)$$
113	112	a1dd	$$⊢\neg \left(\left(\neg \exists y\phi \to y\in \mathrm{V}\right)\to \left(\left(\neg \exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow y\in \mathrm{V}\right)\right)\to \left(\neg \exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \top \right)\right)\right)\right)\to \left(\neg \left(\neg \exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow y\in \mathrm{V}\right)\right)\to \left(\left(\neg \exists y\phi \to y\in \mathrm{V}\right)\to \left(\left(\neg \exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow y\in \mathrm{V}\right)\right)\to \left(\neg \exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \top \right)\right)\right)\right)\right)$$
114	102 113	mt3d	$$⊢\neg \left(\left(\neg \exists y\phi \to y\in \mathrm{V}\right)\to \left(\left(\neg \exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow y\in \mathrm{V}\right)\right)\to \left(\neg \exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \top \right)\right)\right)\right)\to \left(\neg \exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow y\in \mathrm{V}\right)\right)$$
115	108 114	syld	$$⊢\neg \left(\left(\neg \exists y\phi \to y\in \mathrm{V}\right)\to \left(\left(\neg \exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow y\in \mathrm{V}\right)\right)\to \left(\neg \exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \top \right)\right)\right)\right)\to \left(\neg \perp \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow y\in \mathrm{V}\right)\right)$$
116		id	$$⊢\neg \left(\neg \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow y\in \mathrm{V}\right)\vee \neg y\in \mathrm{V}\right)\to \neg \left(\neg \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow y\in \mathrm{V}\right)\vee \neg y\in \mathrm{V}\right)$$
117	116	notornotel2	$$⊢\neg \left(\neg \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow y\in \mathrm{V}\right)\vee \neg y\in \mathrm{V}\right)\to y\in \mathrm{V}$$
118	117	a1i	$$⊢\neg \left(\left(\neg \exists y\phi \to y\in \mathrm{V}\right)\to \left(\left(\neg \exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow y\in \mathrm{V}\right)\right)\to \left(\neg \exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \top \right)\right)\right)\right)\to \left(\neg \left(\neg \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow y\in \mathrm{V}\right)\vee \neg y\in \mathrm{V}\right)\to y\in \mathrm{V}\right)$$
119	116	notornotel1	$$⊢\neg \left(\neg \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow y\in \mathrm{V}\right)\vee \neg y\in \mathrm{V}\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow y\in \mathrm{V}\right)$$
120	119	a1i	$$⊢\neg \left(\left(\neg \exists y\phi \to y\in \mathrm{V}\right)\to \left(\left(\neg \exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow y\in \mathrm{V}\right)\right)\to \left(\neg \exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \top \right)\right)\right)\right)\to \left(\neg \left(\neg \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow y\in \mathrm{V}\right)\vee \neg y\in \mathrm{V}\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow y\in \mathrm{V}\right)\right)$$
121		tsbi3	$$⊢\neg \left(\left(\neg \exists y\phi \to y\in \mathrm{V}\right)\to \left(\left(\neg \exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow y\in \mathrm{V}\right)\right)\to \left(\neg \exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \top \right)\right)\right)\right)\to \left(\left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\vee \neg y\in \mathrm{V}\right)\vee \neg \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow y\in \mathrm{V}\right)\right)$$
122	121	a1d	$$⊢\neg \left(\left(\neg \exists y\phi \to y\in \mathrm{V}\right)\to \left(\left(\neg \exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow y\in \mathrm{V}\right)\right)\to \left(\neg \exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \top \right)\right)\right)\right)\to \left(\neg \left(\neg \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow y\in \mathrm{V}\right)\vee \neg y\in \mathrm{V}\right)\to \left(\left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\vee \neg y\in \mathrm{V}\right)\vee \neg \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow y\in \mathrm{V}\right)\right)\right)$$
123	120 122	cnfn2dd	$$⊢\neg \left(\left(\neg \exists y\phi \to y\in \mathrm{V}\right)\to \left(\left(\neg \exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow y\in \mathrm{V}\right)\right)\to \left(\neg \exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \top \right)\right)\right)\right)\to \left(\neg \left(\neg \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow y\in \mathrm{V}\right)\vee \neg y\in \mathrm{V}\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\vee \neg y\in \mathrm{V}\right)\right)$$
124	118 123	cnfn2dd	$$⊢\neg \left(\left(\neg \exists y\phi \to y\in \mathrm{V}\right)\to \left(\left(\neg \exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow y\in \mathrm{V}\right)\right)\to \left(\neg \exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \top \right)\right)\right)\right)\to \left(\neg \left(\neg \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow y\in \mathrm{V}\right)\vee \neg y\in \mathrm{V}\right)\to y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\right)$$
125		trud	$$⊢\neg \left(\left(\neg \exists y\phi \to y\in \mathrm{V}\right)\to \left(\left(\neg \exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow y\in \mathrm{V}\right)\right)\to \left(\neg \exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \top \right)\right)\right)\right)\to \top$$
126	125	a1d	$$⊢\neg \left(\left(\neg \exists y\phi \to y\in \mathrm{V}\right)\to \left(\left(\neg \exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow y\in \mathrm{V}\right)\right)\to \left(\neg \exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \top \right)\right)\right)\right)\to \left(\neg \left(\neg \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow y\in \mathrm{V}\right)\vee \neg y\in \mathrm{V}\right)\to \top \right)$$
127		tsbi1	$$⊢\neg \left(\left(\neg \exists y\phi \to y\in \mathrm{V}\right)\to \left(\left(\neg \exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow y\in \mathrm{V}\right)\right)\to \left(\neg \exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \top \right)\right)\right)\right)\to \left(\left(\neg y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\vee \neg \top \right)\vee \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \top \right)\right)$$
128	127	a1d	$$⊢\neg \left(\left(\neg \exists y\phi \to y\in \mathrm{V}\right)\to \left(\left(\neg \exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow y\in \mathrm{V}\right)\right)\to \left(\neg \exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \top \right)\right)\right)\right)\to \left(\neg \left(\neg \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow y\in \mathrm{V}\right)\vee \neg y\in \mathrm{V}\right)\to \left(\left(\neg y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\vee \neg \top \right)\vee \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \top \right)\right)\right)$$
129	128	or32dd	$$⊢\neg \left(\left(\neg \exists y\phi \to y\in \mathrm{V}\right)\to \left(\left(\neg \exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow y\in \mathrm{V}\right)\right)\to \left(\neg \exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \top \right)\right)\right)\right)\to \left(\neg \left(\neg \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow y\in \mathrm{V}\right)\vee \neg y\in \mathrm{V}\right)\to \left(\left(\neg y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\vee \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \top \right)\right)\vee \neg \top \right)\right)$$
130	126 129	cnfn2dd	$$⊢\neg \left(\left(\neg \exists y\phi \to y\in \mathrm{V}\right)\to \left(\left(\neg \exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow y\in \mathrm{V}\right)\right)\to \left(\neg \exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \top \right)\right)\right)\right)\to \left(\neg \left(\neg \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow y\in \mathrm{V}\right)\vee \neg y\in \mathrm{V}\right)\to \left(\neg y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\vee \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \top \right)\right)\right)$$
131	124 130	cnfn1dd	$$⊢\neg \left(\left(\neg \exists y\phi \to y\in \mathrm{V}\right)\to \left(\left(\neg \exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow y\in \mathrm{V}\right)\right)\to \left(\neg \exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \top \right)\right)\right)\right)\to \left(\neg \left(\neg \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow y\in \mathrm{V}\right)\vee \neg y\in \mathrm{V}\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \top \right)\right)$$
132	131	a1dd	$$⊢\neg \left(\left(\neg \exists y\phi \to y\in \mathrm{V}\right)\to \left(\left(\neg \exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow y\in \mathrm{V}\right)\right)\to \left(\neg \exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \top \right)\right)\right)\right)\to \left(\neg \left(\neg \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow y\in \mathrm{V}\right)\vee \neg y\in \mathrm{V}\right)\to \left(\neg \exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \top \right)\right)\right)$$
133	132	a1dd	$$⊢\neg \left(\left(\neg \exists y\phi \to y\in \mathrm{V}\right)\to \left(\left(\neg \exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow y\in \mathrm{V}\right)\right)\to \left(\neg \exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \top \right)\right)\right)\right)\to \left(\neg \left(\neg \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow y\in \mathrm{V}\right)\vee \neg y\in \mathrm{V}\right)\to \left(\left(\neg \exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow y\in \mathrm{V}\right)\right)\to \left(\neg \exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \top \right)\right)\right)\right)$$
134		ax-1	$$⊢\neg \left(\left(\neg \exists y\phi \to y\in \mathrm{V}\right)\to \left(\left(\neg \exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow y\in \mathrm{V}\right)\right)\to \left(\neg \exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \top \right)\right)\right)\right)\to \left(\neg \left(\neg \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow y\in \mathrm{V}\right)\vee \neg y\in \mathrm{V}\right)\to \neg \left(\left(\neg \exists y\phi \to y\in \mathrm{V}\right)\to \left(\left(\neg \exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow y\in \mathrm{V}\right)\right)\to \left(\neg \exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \top \right)\right)\right)\right)\right)$$
135		tsim3	$$⊢\neg \left(\left(\neg \exists y\phi \to y\in \mathrm{V}\right)\to \left(\left(\neg \exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow y\in \mathrm{V}\right)\right)\to \left(\neg \exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \top \right)\right)\right)\right)\to \left(\neg \left(\left(\neg \exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow y\in \mathrm{V}\right)\right)\to \left(\neg \exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \top \right)\right)\right)\vee \left(\left(\neg \exists y\phi \to y\in \mathrm{V}\right)\to \left(\left(\neg \exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow y\in \mathrm{V}\right)\right)\to \left(\neg \exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \top \right)\right)\right)\right)\right)$$
136	135	a1d	$$⊢\neg \left(\left(\neg \exists y\phi \to y\in \mathrm{V}\right)\to \left(\left(\neg \exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow y\in \mathrm{V}\right)\right)\to \left(\neg \exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \top \right)\right)\right)\right)\to \left(\neg \left(\neg \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow y\in \mathrm{V}\right)\vee \neg y\in \mathrm{V}\right)\to \left(\neg \left(\left(\neg \exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow y\in \mathrm{V}\right)\right)\to \left(\neg \exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \top \right)\right)\right)\vee \left(\left(\neg \exists y\phi \to y\in \mathrm{V}\right)\to \left(\left(\neg \exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow y\in \mathrm{V}\right)\right)\to \left(\neg \exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \top \right)\right)\right)\right)\right)\right)$$
137	134 136	cnf2dd	$$⊢\neg \left(\left(\neg \exists y\phi \to y\in \mathrm{V}\right)\to \left(\left(\neg \exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow y\in \mathrm{V}\right)\right)\to \left(\neg \exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \top \right)\right)\right)\right)\to \left(\neg \left(\neg \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow y\in \mathrm{V}\right)\vee \neg y\in \mathrm{V}\right)\to \neg \left(\left(\neg \exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow y\in \mathrm{V}\right)\right)\to \left(\neg \exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \top \right)\right)\right)\right)$$
138	133 137	contrd	$$⊢\neg \left(\left(\neg \exists y\phi \to y\in \mathrm{V}\right)\to \left(\left(\neg \exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow y\in \mathrm{V}\right)\right)\to \left(\neg \exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \top \right)\right)\right)\right)\to \left(\neg \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow y\in \mathrm{V}\right)\vee \neg y\in \mathrm{V}\right)$$
139	138	a1d	$$⊢\neg \left(\left(\neg \exists y\phi \to y\in \mathrm{V}\right)\to \left(\left(\neg \exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow y\in \mathrm{V}\right)\right)\to \left(\neg \exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \top \right)\right)\right)\right)\to \left(\neg \perp \to \left(\neg \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow y\in \mathrm{V}\right)\vee \neg y\in \mathrm{V}\right)\right)$$
140	115 139	cnfn1dd	$$⊢\neg \left(\left(\neg \exists y\phi \to y\in \mathrm{V}\right)\to \left(\left(\neg \exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow y\in \mathrm{V}\right)\right)\to \left(\neg \exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \top \right)\right)\right)\right)\to \left(\neg \perp \to \neg y\in \mathrm{V}\right)$$
141	110 140	contrd	$$⊢\neg \left(\left(\neg \exists y\phi \to y\in \mathrm{V}\right)\to \left(\left(\neg \exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow y\in \mathrm{V}\right)\right)\to \left(\neg \exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \top \right)\right)\right)\right)\to \perp$$
142	141	efald2	$$⊢\left(\neg \exists y\phi \to y\in \mathrm{V}\right)\to \left(\left(\neg \exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow y\in \mathrm{V}\right)\right)\to \left(\neg \exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \top \right)\right)\right)$$
143	101 142	ax-mp	$$⊢\left(\neg \exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow y\in \mathrm{V}\right)\right)\to \left(\neg \exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \top \right)\right)$$
144	13 143	ax-mp	$$⊢\neg \exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \top \right)$$
145		ax-1	$$⊢\neg \left(\left(\neg \exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \top \right)\right)\to \left(\neg \exists y\phi \to \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)\right)\to \left(\neg \perp \to \neg \left(\left(\neg \exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \top \right)\right)\to \left(\neg \exists y\phi \to \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)\right)\right)$$
146		tsim3	$$⊢\neg \left(\left(\neg \exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \top \right)\right)\to \left(\neg \exists y\phi \to \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)\right)\to \left(\neg \left(\neg \exists y\phi \to \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)\vee \left(\left(\neg \exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \top \right)\right)\to \left(\neg \exists y\phi \to \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)\right)\right)$$
147	146	a1d	$$⊢\neg \left(\left(\neg \exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \top \right)\right)\to \left(\neg \exists y\phi \to \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)\right)\to \left(\neg \perp \to \left(\neg \left(\neg \exists y\phi \to \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)\vee \left(\left(\neg \exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \top \right)\right)\to \left(\neg \exists y\phi \to \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)\right)\right)\right)$$
148	145 147	cnf2dd	$$⊢\neg \left(\left(\neg \exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \top \right)\right)\to \left(\neg \exists y\phi \to \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)\right)\to \left(\neg \perp \to \neg \left(\neg \exists y\phi \to \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)\right)$$
149		tsim2	$$⊢\neg \left(\left(\neg \exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \top \right)\right)\to \left(\neg \exists y\phi \to \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)\right)\to \left(\neg \exists y\phi \vee \left(\neg \exists y\phi \to \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)\right)$$
150	149	a1d	$$⊢\neg \left(\left(\neg \exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \top \right)\right)\to \left(\neg \exists y\phi \to \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)\right)\to \left(\neg \perp \to \left(\neg \exists y\phi \vee \left(\neg \exists y\phi \to \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)\right)\right)$$
151	148 150	cnf2dd	$$⊢\neg \left(\left(\neg \exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \top \right)\right)\to \left(\neg \exists y\phi \to \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)\right)\to \left(\neg \perp \to \neg \exists y\phi \right)$$
152		tsim2	$$⊢\neg \left(\left(\neg \exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \top \right)\right)\to \left(\neg \exists y\phi \to \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)\right)\to \left(\left(\neg \exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \top \right)\right)\vee \left(\left(\neg \exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \top \right)\right)\to \left(\neg \exists y\phi \to \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)\right)\right)$$
153	152	a1d	$$⊢\neg \left(\left(\neg \exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \top \right)\right)\to \left(\neg \exists y\phi \to \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)\right)\to \left(\neg \perp \to \left(\left(\neg \exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \top \right)\right)\vee \left(\left(\neg \exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \top \right)\right)\to \left(\neg \exists y\phi \to \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)\right)\right)\right)$$
154	145 153	cnf2dd	$$⊢\neg \left(\left(\neg \exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \top \right)\right)\to \left(\neg \exists y\phi \to \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)\right)\to \left(\neg \perp \to \left(\neg \exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \top \right)\right)\right)$$
155	151 154	mpdd	$$⊢\neg \left(\left(\neg \exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \top \right)\right)\to \left(\neg \exists y\phi \to \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)\right)\to \left(\neg \perp \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \top \right)\right)$$
156		id	$$⊢\neg \left(\left(\neg \exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \top \right)\right)\to \left(\neg \exists y\phi \to \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)\right)\to \neg \left(\left(\neg \exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \top \right)\right)\to \left(\neg \exists y\phi \to \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)\right)$$
157		id	$$⊢\neg \left(\exists y\phi \to \psi \right)\to \neg \left(\exists y\phi \to \psi \right)$$
158	157	a1i	$$⊢\neg \left(\left(\neg \exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \top \right)\right)\to \left(\neg \exists y\phi \to \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)\right)\to \left(\neg \left(\exists y\phi \to \psi \right)\to \neg \left(\exists y\phi \to \psi \right)\right)$$
159		tsim2	$$⊢\neg \left(\left(\neg \exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \top \right)\right)\to \left(\neg \exists y\phi \to \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)\right)\to \left(\exists y\phi \vee \left(\exists y\phi \to \psi \right)\right)$$
160	159	a1d	$$⊢\neg \left(\left(\neg \exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \top \right)\right)\to \left(\neg \exists y\phi \to \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)\right)\to \left(\neg \left(\exists y\phi \to \psi \right)\to \left(\exists y\phi \vee \left(\exists y\phi \to \psi \right)\right)\right)$$
161	158 160	cnf2dd	$$⊢\neg \left(\left(\neg \exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \top \right)\right)\to \left(\neg \exists y\phi \to \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)\right)\to \left(\neg \left(\exists y\phi \to \psi \right)\to \exists y\phi \right)$$
162	149	a1d	$$⊢\neg \left(\left(\neg \exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \top \right)\right)\to \left(\neg \exists y\phi \to \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)\right)\to \left(\neg \left(\exists y\phi \to \psi \right)\to \left(\neg \exists y\phi \vee \left(\neg \exists y\phi \to \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)\right)\right)$$
163	161 162	cnfn1dd	$$⊢\neg \left(\left(\neg \exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \top \right)\right)\to \left(\neg \exists y\phi \to \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)\right)\to \left(\neg \left(\exists y\phi \to \psi \right)\to \left(\neg \exists y\phi \to \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)\right)$$
164	163	a1dd	$$⊢\neg \left(\left(\neg \exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \top \right)\right)\to \left(\neg \exists y\phi \to \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)\right)\to \left(\neg \left(\exists y\phi \to \psi \right)\to \left(\left(\neg \exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \top \right)\right)\to \left(\neg \exists y\phi \to \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)\right)\right)$$
165	156 164	mt3d	$$⊢\neg \left(\left(\neg \exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \top \right)\right)\to \left(\neg \exists y\phi \to \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)\right)\to \left(\exists y\phi \to \psi \right)$$
166	165	a1d	$$⊢\neg \left(\left(\neg \exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \top \right)\right)\to \left(\neg \exists y\phi \to \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)\right)\to \left(\neg \perp \to \left(\exists y\phi \to \psi \right)\right)$$
167		tsim3	$$⊢\neg \left(\left(\neg \exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \top \right)\right)\to \left(\neg \exists y\phi \to \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)\right)\to \left(\neg \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\vee \left(\neg \exists y\phi \to \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)\right)$$
168	167	a1d	$$⊢\neg \left(\left(\neg \exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \top \right)\right)\to \left(\neg \exists y\phi \to \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)\right)\to \left(\neg \perp \to \left(\neg \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\vee \left(\neg \exists y\phi \to \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)\right)\right)$$
169	148 168	cnf2dd	$$⊢\neg \left(\left(\neg \exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \top \right)\right)\to \left(\neg \exists y\phi \to \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)\right)\to \left(\neg \perp \to \neg \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)$$
170		tsim3	$$⊢\neg \left(\left(\neg \exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \top \right)\right)\to \left(\neg \exists y\phi \to \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)\right)\to \left(\neg \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\vee \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)$$
171	170	a1d	$$⊢\neg \left(\left(\neg \exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \top \right)\right)\to \left(\neg \exists y\phi \to \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)\right)\to \left(\neg \perp \to \left(\neg \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\vee \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)\right)$$
172	169 171	cnf2dd	$$⊢\neg \left(\left(\neg \exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \top \right)\right)\to \left(\neg \exists y\phi \to \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)\right)\to \left(\neg \perp \to \neg \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)$$
173		tsbi1	$$⊢\neg \left(\left(\neg \exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \top \right)\right)\to \left(\neg \exists y\phi \to \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)\right)\to \left(\left(\neg y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\vee \neg \left(\exists y\phi \to \psi \right)\right)\vee \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)$$
174	173	a1d	$$⊢\neg \left(\left(\neg \exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \top \right)\right)\to \left(\neg \exists y\phi \to \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)\right)\to \left(\neg \perp \to \left(\left(\neg y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\vee \neg \left(\exists y\phi \to \psi \right)\right)\vee \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)$$
175	172 174	cnf2dd	$$⊢\neg \left(\left(\neg \exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \top \right)\right)\to \left(\neg \exists y\phi \to \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)\right)\to \left(\neg \perp \to \left(\neg y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\vee \neg \left(\exists y\phi \to \psi \right)\right)\right)$$
176	166 175	cnfn2dd	$$⊢\neg \left(\left(\neg \exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \top \right)\right)\to \left(\neg \exists y\phi \to \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)\right)\to \left(\neg \perp \to \neg y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\right)$$
177		trud	$$⊢\neg \left(\left(\neg \exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \top \right)\right)\to \left(\neg \exists y\phi \to \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)\right)\to \top$$
178	177	a1d	$$⊢\neg \left(\left(\neg \exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \top \right)\right)\to \left(\neg \exists y\phi \to \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)\right)\to \left(\neg \perp \to \top \right)$$
179		tsbi3	$$⊢\neg \left(\left(\neg \exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \top \right)\right)\to \left(\neg \exists y\phi \to \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)\right)\to \left(\left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\vee \neg \top \right)\vee \neg \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \top \right)\right)$$
180	179	a1d	$$⊢\neg \left(\left(\neg \exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \top \right)\right)\to \left(\neg \exists y\phi \to \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)\right)\to \left(\neg \perp \to \left(\left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\vee \neg \top \right)\vee \neg \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \top \right)\right)\right)$$
181	180	or32dd	$$⊢\neg \left(\left(\neg \exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \top \right)\right)\to \left(\neg \exists y\phi \to \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)\right)\to \left(\neg \perp \to \left(\left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\vee \neg \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \top \right)\right)\vee \neg \top \right)\right)$$
182	178 181	cnfn2dd	$$⊢\neg \left(\left(\neg \exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \top \right)\right)\to \left(\neg \exists y\phi \to \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)\right)\to \left(\neg \perp \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\vee \neg \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \top \right)\right)\right)$$
183	176 182	cnf1dd	$$⊢\neg \left(\left(\neg \exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \top \right)\right)\to \left(\neg \exists y\phi \to \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)\right)\to \left(\neg \perp \to \neg \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \top \right)\right)$$
184	155 183	contrd	$$⊢\neg \left(\left(\neg \exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \top \right)\right)\to \left(\neg \exists y\phi \to \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)\right)\to \perp$$
185	184	efald2	$$⊢\left(\neg \exists y\phi \to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \top \right)\right)\to \left(\neg \exists y\phi \to \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)\right)$$
186	144 185	ax-mp	$$⊢\neg \exists y\phi \to \left(y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)\right)$$
187	100 186	pm2.61i	$$⊢y=f\left(x\right)\to \left(y\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\leftrightarrow \left(\exists y\phi \to \psi \right)\right)$$
188	19 2 187	ac6s3f	$$⊢\forall x\in A\exists yy\in if\left(\exists y\phi ,\left\{y|\phi \right\},\mathrm{V}\right)\to \exists f\forall x\in A\left(\exists y\phi \to \psi \right)$$
189	17 188	ax-mp	$$⊢\exists f\forall x\in A\left(\exists y\phi \to \psi \right)$$