mpobi123f

Description: Equality deduction for maps-to notations with two arguments. (Contributed by Giovanni Mascellani, 10-Apr-2018)

	Ref	Expression
Hypotheses	mpobi123f.1	$⊢ \underline{Ⅎ} x A$
	mpobi123f.2	$⊢ \underline{Ⅎ} x B$
	mpobi123f.3	$⊢ \underline{Ⅎ} y A$
	mpobi123f.4	$⊢ \underline{Ⅎ} y B$
	mpobi123f.5	$⊢ \underline{Ⅎ} y C$
	mpobi123f.6	$⊢ \underline{Ⅎ} y D$
	mpobi123f.7	$⊢ \underline{Ⅎ} x C$
	mpobi123f.8	$⊢ \underline{Ⅎ} x D$
Assertion	mpobi123f	$⊢ ((A = B \land C = D) \land \forall x \in A \forall y \in C E = F) \to (x \in A, y \in C ⟼ E) = (x \in B, y \in D ⟼ F)$

Proof

Step	Hyp	Ref	Expression
1		mpobi123f.1	$⊢ \underline{Ⅎ} x A$
2		mpobi123f.2	$⊢ \underline{Ⅎ} x B$
3		mpobi123f.3	$⊢ \underline{Ⅎ} y A$
4		mpobi123f.4	$⊢ \underline{Ⅎ} y B$
5		mpobi123f.5	$⊢ \underline{Ⅎ} y C$
6		mpobi123f.6	$⊢ \underline{Ⅎ} y D$
7		mpobi123f.7	$⊢ \underline{Ⅎ} x C$
8		mpobi123f.8	$⊢ \underline{Ⅎ} x D$
9	1 2	nfeq	$⊢ Ⅎ x A = B$
10		eleq2	$⊢ A = B \to (x \in A \leftrightarrow x \in B)$
11	9 10	alrimi	$⊢ A = B \to \forall x (x \in A \leftrightarrow x \in B)$
12	3	nfcri	$⊢ Ⅎ y x \in A$
13	4	nfcri	$⊢ Ⅎ y x \in B$
14	12 13	nfbi	$⊢ Ⅎ y (x \in A \leftrightarrow x \in B)$
15		ax-5	$⊢ (x \in A \leftrightarrow x \in B) \to \forall z (x \in A \leftrightarrow x \in B)$
16	14 15	alrimi	$⊢ (x \in A \leftrightarrow x \in B) \to \forall y \forall z (x \in A \leftrightarrow x \in B)$
17	11 16	sylg	$⊢ A = B \to \forall x \forall y \forall z (x \in A \leftrightarrow x \in B)$
18	5 6	nfeq	$⊢ Ⅎ y C = D$
19		eleq2	$⊢ C = D \to (y \in C \leftrightarrow y \in D)$
20	18 19	alrimi	$⊢ C = D \to \forall y (y \in C \leftrightarrow y \in D)$
21		ax-5	$⊢ (y \in C \leftrightarrow y \in D) \to \forall z (y \in C \leftrightarrow y \in D)$
22	21	alimi	$⊢ \forall y (y \in C \leftrightarrow y \in D) \to \forall y \forall z (y \in C \leftrightarrow y \in D)$
23	7	nfcri	$⊢ Ⅎ x y \in C$
24	8	nfcri	$⊢ Ⅎ x y \in D$
25	23 24	nfbi	$⊢ Ⅎ x (y \in C \leftrightarrow y \in D)$
26	25	nfal	$⊢ Ⅎ x \forall z (y \in C \leftrightarrow y \in D)$
27	26	nfal	$⊢ Ⅎ x \forall y \forall z (y \in C \leftrightarrow y \in D)$
28	27	nf5ri	$⊢ \forall y \forall z (y \in C \leftrightarrow y \in D) \to \forall x \forall y \forall z (y \in C \leftrightarrow y \in D)$
29	20 22 28	3syl	$⊢ C = D \to \forall x \forall y \forall z (y \in C \leftrightarrow y \in D)$
30		id	$⊢ ((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D)) \to ((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D))$
31	30	alanimi	$⊢ (\forall z (x \in A \leftrightarrow x \in B) \land \forall z (y \in C \leftrightarrow y \in D)) \to \forall z ((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D))$
32	31	alanimi	$⊢ (\forall y \forall z (x \in A \leftrightarrow x \in B) \land \forall y \forall z (y \in C \leftrightarrow y \in D)) \to \forall y \forall z ((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D))$
33	32	alanimi	$⊢ (\forall x \forall y \forall z (x \in A \leftrightarrow x \in B) \land \forall x \forall y \forall z (y \in C \leftrightarrow y \in D)) \to \forall x \forall y \forall z ((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D))$
34	17 29 33	syl2an	$⊢ (A = B \land C = D) \to \forall x \forall y \forall z ((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D))$
35		eqeq2	$⊢ E = F \to (z = E \leftrightarrow z = F)$
36	35	alrimiv	$⊢ E = F \to \forall z (z = E \leftrightarrow z = F)$
37	36	2ralimi	$⊢ \forall x \in A \forall y \in C E = F \to \forall x \in A \forall y \in C \forall z (z = E \leftrightarrow z = F)$
38		hbra1	$⊢ \forall y \in C \forall z (z = E \leftrightarrow z = F) \to \forall y \forall y \in C \forall z (z = E \leftrightarrow z = F)$
39		rsp	$⊢ \forall y \in C \forall z (z = E \leftrightarrow z = F) \to (y \in C \to \forall z (z = E \leftrightarrow z = F))$
40	38 39	alrimih	$⊢ \forall y \in C \forall z (z = E \leftrightarrow z = F) \to \forall y (y \in C \to \forall z (z = E \leftrightarrow z = F))$
41		19.21v	$⊢ \forall z (y \in C \to (z = E \leftrightarrow z = F)) \leftrightarrow (y \in C \to \forall z (z = E \leftrightarrow z = F))$
42	41	albii	$⊢ \forall y \forall z (y \in C \to (z = E \leftrightarrow z = F)) \leftrightarrow \forall y (y \in C \to \forall z (z = E \leftrightarrow z = F))$
43	40 42	sylibr	$⊢ \forall y \in C \forall z (z = E \leftrightarrow z = F) \to \forall y \forall z (y \in C \to (z = E \leftrightarrow z = F))$
44	43	ralimi	$⊢ \forall x \in A \forall y \in C \forall z (z = E \leftrightarrow z = F) \to \forall x \in A \forall y \forall z (y \in C \to (z = E \leftrightarrow z = F))$
45		hbra1	$⊢ \forall x \in A \forall y \forall z (y \in C \to (z = E \leftrightarrow z = F)) \to \forall x \forall x \in A \forall y \forall z (y \in C \to (z = E \leftrightarrow z = F))$
46		rsp	$⊢ \forall x \in A \forall y \forall z (y \in C \to (z = E \leftrightarrow z = F)) \to (x \in A \to \forall y \forall z (y \in C \to (z = E \leftrightarrow z = F)))$
47	45 46	alrimih	$⊢ \forall x \in A \forall y \forall z (y \in C \to (z = E \leftrightarrow z = F)) \to \forall x (x \in A \to \forall y \forall z (y \in C \to (z = E \leftrightarrow z = F)))$
48		19.21v	$⊢ \forall z (x \in A \to (y \in C \to (z = E \leftrightarrow z = F))) \leftrightarrow (x \in A \to \forall z (y \in C \to (z = E \leftrightarrow z = F)))$
49	48	2albii	$⊢ \forall x \forall y \forall z (x \in A \to (y \in C \to (z = E \leftrightarrow z = F))) \leftrightarrow \forall x \forall y (x \in A \to \forall z (y \in C \to (z = E \leftrightarrow z = F)))$
50	12	19.21	$⊢ \forall y (x \in A \to \forall z (y \in C \to (z = E \leftrightarrow z = F))) \leftrightarrow (x \in A \to \forall y \forall z (y \in C \to (z = E \leftrightarrow z = F)))$
51	50	albii	$⊢ \forall x \forall y (x \in A \to \forall z (y \in C \to (z = E \leftrightarrow z = F))) \leftrightarrow \forall x (x \in A \to \forall y \forall z (y \in C \to (z = E \leftrightarrow z = F)))$
52	49 51	sylbbr	$⊢ \forall x (x \in A \to \forall y \forall z (y \in C \to (z = E \leftrightarrow z = F))) \to \forall x \forall y \forall z (x \in A \to (y \in C \to (z = E \leftrightarrow z = F)))$
53	44 47 52	3syl	$⊢ \forall x \in A \forall y \in C \forall z (z = E \leftrightarrow z = F) \to \forall x \forall y \forall z (x \in A \to (y \in C \to (z = E \leftrightarrow z = F)))$
54	37 53	syl	$⊢ \forall x \in A \forall y \in C E = F \to \forall x \forall y \forall z (x \in A \to (y \in C \to (z = E \leftrightarrow z = F)))$
55		id	$⊢ (((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D)) \land (x \in A \to (y \in C \to (z = E \leftrightarrow z = F)))) \to (((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D)) \land (x \in A \to (y \in C \to (z = E \leftrightarrow z = F))))$
56	55	alanimi	$⊢ (\forall z ((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D)) \land \forall z (x \in A \to (y \in C \to (z = E \leftrightarrow z = F)))) \to \forall z (((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D)) \land (x \in A \to (y \in C \to (z = E \leftrightarrow z = F))))$
57	56	alanimi	$⊢ (\forall y \forall z ((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D)) \land \forall y \forall z (x \in A \to (y \in C \to (z = E \leftrightarrow z = F)))) \to \forall y \forall z (((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D)) \land (x \in A \to (y \in C \to (z = E \leftrightarrow z = F))))$
58	57	alanimi	$⊢ (\forall x \forall y \forall z ((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D)) \land \forall x \forall y \forall z (x \in A \to (y \in C \to (z = E \leftrightarrow z = F)))) \to \forall x \forall y \forall z (((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D)) \land (x \in A \to (y \in C \to (z = E \leftrightarrow z = F))))$
59	34 54 58	syl2an	$⊢ ((A = B \land C = D) \land \forall x \in A \forall y \in C E = F) \to \forall x \forall y \forall z (((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D)) \land (x \in A \to (y \in C \to (z = E \leftrightarrow z = F))))$
60		tsan2	$⊢ \neg ((((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D)) \land (x \in A \to (y \in C \to (z = E \leftrightarrow z = F)))) \to (((x \in A \land y \in C) \land z = E) \leftrightarrow ((x \in B \land y \in D) \land z = F))) \to (x \in A \lor \neg (x \in A \land y \in C))$
61	60	ord	$⊢ \neg ((((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D)) \land (x \in A \to (y \in C \to (z = E \leftrightarrow z = F)))) \to (((x \in A \land y \in C) \land z = E) \leftrightarrow ((x \in B \land y \in D) \land z = F))) \to (\neg x \in A \to \neg (x \in A \land y \in C))$
62		tsan2	$⊢ \neg ((((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D)) \land (x \in A \to (y \in C \to (z = E \leftrightarrow z = F)))) \to (((x \in A \land y \in C) \land z = E) \leftrightarrow ((x \in B \land y \in D) \land z = F))) \to ((x \in A \land y \in C) \lor \neg ((x \in A \land y \in C) \land z = E))$
63	62	a1d	$⊢ \neg ((((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D)) \land (x \in A \to (y \in C \to (z = E \leftrightarrow z = F)))) \to (((x \in A \land y \in C) \land z = E) \leftrightarrow ((x \in B \land y \in D) \land z = F))) \to (\neg x \in A \to ((x \in A \land y \in C) \lor \neg ((x \in A \land y \in C) \land z = E)))$
64	61 63	cnf1dd	$⊢ \neg ((((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D)) \land (x \in A \to (y \in C \to (z = E \leftrightarrow z = F)))) \to (((x \in A \land y \in C) \land z = E) \leftrightarrow ((x \in B \land y \in D) \land z = F))) \to (\neg x \in A \to \neg ((x \in A \land y \in C) \land z = E))$
65		tsbi2	$⊢ \neg ((((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D)) \land (x \in A \to (y \in C \to (z = E \leftrightarrow z = F)))) \to (((x \in A \land y \in C) \land z = E) \leftrightarrow ((x \in B \land y \in D) \land z = F))) \to ((((x \in A \land y \in C) \land z = E) \lor ((x \in B \land y \in D) \land z = F)) \lor (((x \in A \land y \in C) \land z = E) \leftrightarrow ((x \in B \land y \in D) \land z = F)))$
66	65	ord	$⊢ \neg ((((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D)) \land (x \in A \to (y \in C \to (z = E \leftrightarrow z = F)))) \to (((x \in A \land y \in C) \land z = E) \leftrightarrow ((x \in B \land y \in D) \land z = F))) \to (\neg (((x \in A \land y \in C) \land z = E) \lor ((x \in B \land y \in D) \land z = F)) \to (((x \in A \land y \in C) \land z = E) \leftrightarrow ((x \in B \land y \in D) \land z = F)))$
67	66	a1dd	$⊢ \neg ((((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D)) \land (x \in A \to (y \in C \to (z = E \leftrightarrow z = F)))) \to (((x \in A \land y \in C) \land z = E) \leftrightarrow ((x \in B \land y \in D) \land z = F))) \to (\neg (((x \in A \land y \in C) \land z = E) \lor ((x \in B \land y \in D) \land z = F)) \to ((((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D)) \land (x \in A \to (y \in C \to (z = E \leftrightarrow z = F)))) \to (((x \in A \land y \in C) \land z = E) \leftrightarrow ((x \in B \land y \in D) \land z = F))))$
68		ax-1	$⊢ \neg ((((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D)) \land (x \in A \to (y \in C \to (z = E \leftrightarrow z = F)))) \to (((x \in A \land y \in C) \land z = E) \leftrightarrow ((x \in B \land y \in D) \land z = F))) \to (\neg (((x \in A \land y \in C) \land z = E) \lor ((x \in B \land y \in D) \land z = F)) \to \neg ((((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D)) \land (x \in A \to (y \in C \to (z = E \leftrightarrow z = F)))) \to (((x \in A \land y \in C) \land z = E) \leftrightarrow ((x \in B \land y \in D) \land z = F))))$
69	67 68	contrd	$⊢ \neg ((((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D)) \land (x \in A \to (y \in C \to (z = E \leftrightarrow z = F)))) \to (((x \in A \land y \in C) \land z = E) \leftrightarrow ((x \in B \land y \in D) \land z = F))) \to (((x \in A \land y \in C) \land z = E) \lor ((x \in B \land y \in D) \land z = F))$
70	69	a1d	$⊢ \neg ((((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D)) \land (x \in A \to (y \in C \to (z = E \leftrightarrow z = F)))) \to (((x \in A \land y \in C) \land z = E) \leftrightarrow ((x \in B \land y \in D) \land z = F))) \to (\neg x \in A \to (((x \in A \land y \in C) \land z = E) \lor ((x \in B \land y \in D) \land z = F)))$
71	64 70	cnf1dd	$⊢ \neg ((((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D)) \land (x \in A \to (y \in C \to (z = E \leftrightarrow z = F)))) \to (((x \in A \land y \in C) \land z = E) \leftrightarrow ((x \in B \land y \in D) \land z = F))) \to (\neg x \in A \to ((x \in B \land y \in D) \land z = F))$
72		idd	$⊢ \neg ((((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D)) \land (x \in A \to (y \in C \to (z = E \leftrightarrow z = F)))) \to (((x \in A \land y \in C) \land z = E) \leftrightarrow ((x \in B \land y \in D) \land z = F))) \to (\neg x \in A \to \neg x \in A)$
73		tsan2	$⊢ \neg ((((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D)) \land (x \in A \to (y \in C \to (z = E \leftrightarrow z = F)))) \to (((x \in A \land y \in C) \land z = E) \leftrightarrow ((x \in B \land y \in D) \land z = F))) \to ((x \in A \leftrightarrow x \in B) \lor \neg ((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D)))$
74	73	ord	$⊢ \neg ((((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D)) \land (x \in A \to (y \in C \to (z = E \leftrightarrow z = F)))) \to (((x \in A \land y \in C) \land z = E) \leftrightarrow ((x \in B \land y \in D) \land z = F))) \to (\neg (x \in A \leftrightarrow x \in B) \to \neg ((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D)))$
75		tsan2	$⊢ \neg ((((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D)) \land (x \in A \to (y \in C \to (z = E \leftrightarrow z = F)))) \to (((x \in A \land y \in C) \land z = E) \leftrightarrow ((x \in B \land y \in D) \land z = F))) \to (((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D)) \lor \neg (((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D)) \land (x \in A \to (y \in C \to (z = E \leftrightarrow z = F)))))$
76	75	a1d	$⊢ \neg ((((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D)) \land (x \in A \to (y \in C \to (z = E \leftrightarrow z = F)))) \to (((x \in A \land y \in C) \land z = E) \leftrightarrow ((x \in B \land y \in D) \land z = F))) \to (\neg (x \in A \leftrightarrow x \in B) \to (((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D)) \lor \neg (((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D)) \land (x \in A \to (y \in C \to (z = E \leftrightarrow z = F))))))$
77	74 76	cnf1dd	$⊢ \neg ((((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D)) \land (x \in A \to (y \in C \to (z = E \leftrightarrow z = F)))) \to (((x \in A \land y \in C) \land z = E) \leftrightarrow ((x \in B \land y \in D) \land z = F))) \to (\neg (x \in A \leftrightarrow x \in B) \to \neg (((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D)) \land (x \in A \to (y \in C \to (z = E \leftrightarrow z = F)))))$
78		tsim2	$⊢ \neg ((((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D)) \land (x \in A \to (y \in C \to (z = E \leftrightarrow z = F)))) \to (((x \in A \land y \in C) \land z = E) \leftrightarrow ((x \in B \land y \in D) \land z = F))) \to ((((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D)) \land (x \in A \to (y \in C \to (z = E \leftrightarrow z = F)))) \lor ((((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D)) \land (x \in A \to (y \in C \to (z = E \leftrightarrow z = F)))) \to (((x \in A \land y \in C) \land z = E) \leftrightarrow ((x \in B \land y \in D) \land z = F))))$
79	78	a1d	$⊢ \neg ((((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D)) \land (x \in A \to (y \in C \to (z = E \leftrightarrow z = F)))) \to (((x \in A \land y \in C) \land z = E) \leftrightarrow ((x \in B \land y \in D) \land z = F))) \to (\neg (x \in A \leftrightarrow x \in B) \to ((((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D)) \land (x \in A \to (y \in C \to (z = E \leftrightarrow z = F)))) \lor ((((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D)) \land (x \in A \to (y \in C \to (z = E \leftrightarrow z = F)))) \to (((x \in A \land y \in C) \land z = E) \leftrightarrow ((x \in B \land y \in D) \land z = F)))))$
80	77 79	cnf1dd	$⊢ \neg ((((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D)) \land (x \in A \to (y \in C \to (z = E \leftrightarrow z = F)))) \to (((x \in A \land y \in C) \land z = E) \leftrightarrow ((x \in B \land y \in D) \land z = F))) \to (\neg (x \in A \leftrightarrow x \in B) \to ((((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D)) \land (x \in A \to (y \in C \to (z = E \leftrightarrow z = F)))) \to (((x \in A \land y \in C) \land z = E) \leftrightarrow ((x \in B \land y \in D) \land z = F))))$
81		ax-1	$⊢ \neg ((((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D)) \land (x \in A \to (y \in C \to (z = E \leftrightarrow z = F)))) \to (((x \in A \land y \in C) \land z = E) \leftrightarrow ((x \in B \land y \in D) \land z = F))) \to (\neg (x \in A \leftrightarrow x \in B) \to \neg ((((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D)) \land (x \in A \to (y \in C \to (z = E \leftrightarrow z = F)))) \to (((x \in A \land y \in C) \land z = E) \leftrightarrow ((x \in B \land y \in D) \land z = F))))$
82	80 81	contrd	$⊢ \neg ((((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D)) \land (x \in A \to (y \in C \to (z = E \leftrightarrow z = F)))) \to (((x \in A \land y \in C) \land z = E) \leftrightarrow ((x \in B \land y \in D) \land z = F))) \to (x \in A \leftrightarrow x \in B)$
83	82	a1d	$⊢ \neg ((((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D)) \land (x \in A \to (y \in C \to (z = E \leftrightarrow z = F)))) \to (((x \in A \land y \in C) \land z = E) \leftrightarrow ((x \in B \land y \in D) \land z = F))) \to (\neg x \in A \to (x \in A \leftrightarrow x \in B))$
84		tsbi3	$⊢ \neg ((((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D)) \land (x \in A \to (y \in C \to (z = E \leftrightarrow z = F)))) \to (((x \in A \land y \in C) \land z = E) \leftrightarrow ((x \in B \land y \in D) \land z = F))) \to ((x \in A \lor \neg x \in B) \lor \neg (x \in A \leftrightarrow x \in B))$
85	84	a1d	$⊢ \neg ((((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D)) \land (x \in A \to (y \in C \to (z = E \leftrightarrow z = F)))) \to (((x \in A \land y \in C) \land z = E) \leftrightarrow ((x \in B \land y \in D) \land z = F))) \to (\neg x \in A \to ((x \in A \lor \neg x \in B) \lor \neg (x \in A \leftrightarrow x \in B)))$
86	83 85	cnfn2dd	$⊢ \neg ((((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D)) \land (x \in A \to (y \in C \to (z = E \leftrightarrow z = F)))) \to (((x \in A \land y \in C) \land z = E) \leftrightarrow ((x \in B \land y \in D) \land z = F))) \to (\neg x \in A \to (x \in A \lor \neg x \in B))$
87	72 86	cnf1dd	$⊢ \neg ((((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D)) \land (x \in A \to (y \in C \to (z = E \leftrightarrow z = F)))) \to (((x \in A \land y \in C) \land z = E) \leftrightarrow ((x \in B \land y \in D) \land z = F))) \to (\neg x \in A \to \neg x \in B)$
88		tsan2	$⊢ \neg ((((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D)) \land (x \in A \to (y \in C \to (z = E \leftrightarrow z = F)))) \to (((x \in A \land y \in C) \land z = E) \leftrightarrow ((x \in B \land y \in D) \land z = F))) \to (x \in B \lor \neg (x \in B \land y \in D))$
89	88	a1d	$⊢ \neg ((((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D)) \land (x \in A \to (y \in C \to (z = E \leftrightarrow z = F)))) \to (((x \in A \land y \in C) \land z = E) \leftrightarrow ((x \in B \land y \in D) \land z = F))) \to (\neg x \in A \to (x \in B \lor \neg (x \in B \land y \in D)))$
90	87 89	cnf1dd	$⊢ \neg ((((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D)) \land (x \in A \to (y \in C \to (z = E \leftrightarrow z = F)))) \to (((x \in A \land y \in C) \land z = E) \leftrightarrow ((x \in B \land y \in D) \land z = F))) \to (\neg x \in A \to \neg (x \in B \land y \in D))$
91		tsan2	$⊢ \neg ((((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D)) \land (x \in A \to (y \in C \to (z = E \leftrightarrow z = F)))) \to (((x \in A \land y \in C) \land z = E) \leftrightarrow ((x \in B \land y \in D) \land z = F))) \to ((x \in B \land y \in D) \lor \neg ((x \in B \land y \in D) \land z = F))$
92	91	a1d	$⊢ \neg ((((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D)) \land (x \in A \to (y \in C \to (z = E \leftrightarrow z = F)))) \to (((x \in A \land y \in C) \land z = E) \leftrightarrow ((x \in B \land y \in D) \land z = F))) \to (\neg x \in A \to ((x \in B \land y \in D) \lor \neg ((x \in B \land y \in D) \land z = F)))$
93	90 92	cnf1dd	$⊢ \neg ((((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D)) \land (x \in A \to (y \in C \to (z = E \leftrightarrow z = F)))) \to (((x \in A \land y \in C) \land z = E) \leftrightarrow ((x \in B \land y \in D) \land z = F))) \to (\neg x \in A \to \neg ((x \in B \land y \in D) \land z = F))$
94	71 93	contrd	$⊢ \neg ((((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D)) \land (x \in A \to (y \in C \to (z = E \leftrightarrow z = F)))) \to (((x \in A \land y \in C) \land z = E) \leftrightarrow ((x \in B \land y \in D) \land z = F))) \to x \in A$
95	94	a1d	$⊢ \neg ((((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D)) \land (x \in A \to (y \in C \to (z = E \leftrightarrow z = F)))) \to (((x \in A \land y \in C) \land z = E) \leftrightarrow ((x \in B \land y \in D) \land z = F))) \to (\neg ⊥ \to x \in A)$
96		ax-1	$⊢ \neg ((((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D)) \land (x \in A \to (y \in C \to (z = E \leftrightarrow z = F)))) \to (((x \in A \land y \in C) \land z = E) \leftrightarrow ((x \in B \land y \in D) \land z = F))) \to (\neg ⊥ \to \neg ((((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D)) \land (x \in A \to (y \in C \to (z = E \leftrightarrow z = F)))) \to (((x \in A \land y \in C) \land z = E) \leftrightarrow ((x \in B \land y \in D) \land z = F))))$
97	78	a1d	$⊢ \neg ((((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D)) \land (x \in A \to (y \in C \to (z = E \leftrightarrow z = F)))) \to (((x \in A \land y \in C) \land z = E) \leftrightarrow ((x \in B \land y \in D) \land z = F))) \to (\neg ⊥ \to ((((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D)) \land (x \in A \to (y \in C \to (z = E \leftrightarrow z = F)))) \lor ((((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D)) \land (x \in A \to (y \in C \to (z = E \leftrightarrow z = F)))) \to (((x \in A \land y \in C) \land z = E) \leftrightarrow ((x \in B \land y \in D) \land z = F)))))$
98	96 97	cnf2dd	$⊢ \neg ((((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D)) \land (x \in A \to (y \in C \to (z = E \leftrightarrow z = F)))) \to (((x \in A \land y \in C) \land z = E) \leftrightarrow ((x \in B \land y \in D) \land z = F))) \to (\neg ⊥ \to (((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D)) \land (x \in A \to (y \in C \to (z = E \leftrightarrow z = F)))))$
99		tsan3	$⊢ \neg ((((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D)) \land (x \in A \to (y \in C \to (z = E \leftrightarrow z = F)))) \to (((x \in A \land y \in C) \land z = E) \leftrightarrow ((x \in B \land y \in D) \land z = F))) \to ((x \in A \to (y \in C \to (z = E \leftrightarrow z = F))) \lor \neg (((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D)) \land (x \in A \to (y \in C \to (z = E \leftrightarrow z = F)))))$
100	99	a1d	$⊢ \neg ((((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D)) \land (x \in A \to (y \in C \to (z = E \leftrightarrow z = F)))) \to (((x \in A \land y \in C) \land z = E) \leftrightarrow ((x \in B \land y \in D) \land z = F))) \to (\neg ⊥ \to ((x \in A \to (y \in C \to (z = E \leftrightarrow z = F))) \lor \neg (((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D)) \land (x \in A \to (y \in C \to (z = E \leftrightarrow z = F))))))$
101	98 100	cnfn2dd	$⊢ \neg ((((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D)) \land (x \in A \to (y \in C \to (z = E \leftrightarrow z = F)))) \to (((x \in A \land y \in C) \land z = E) \leftrightarrow ((x \in B \land y \in D) \land z = F))) \to (\neg ⊥ \to (x \in A \to (y \in C \to (z = E \leftrightarrow z = F))))$
102	95 101	mpdd	$⊢ \neg ((((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D)) \land (x \in A \to (y \in C \to (z = E \leftrightarrow z = F)))) \to (((x \in A \land y \in C) \land z = E) \leftrightarrow ((x \in B \land y \in D) \land z = F))) \to (\neg ⊥ \to (y \in C \to (z = E \leftrightarrow z = F)))$
103		notnotr	$⊢ \neg \neg ((x \in B \land y \in D) \land z = F) \to ((x \in B \land y \in D) \land z = F)$
104	103	a1i	$⊢ \neg ((((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D)) \land (x \in A \to (y \in C \to (z = E \leftrightarrow z = F)))) \to (((x \in A \land y \in C) \land z = E) \leftrightarrow ((x \in B \land y \in D) \land z = F))) \to (\neg \neg ((x \in B \land y \in D) \land z = F) \to ((x \in B \land y \in D) \land z = F))$
105	91	a1d	$⊢ \neg ((((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D)) \land (x \in A \to (y \in C \to (z = E \leftrightarrow z = F)))) \to (((x \in A \land y \in C) \land z = E) \leftrightarrow ((x \in B \land y \in D) \land z = F))) \to (\neg \neg ((x \in B \land y \in D) \land z = F) \to ((x \in B \land y \in D) \lor \neg ((x \in B \land y \in D) \land z = F)))$
106	104 105	cnfn2dd	$⊢ \neg ((((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D)) \land (x \in A \to (y \in C \to (z = E \leftrightarrow z = F)))) \to (((x \in A \land y \in C) \land z = E) \leftrightarrow ((x \in B \land y \in D) \land z = F))) \to (\neg \neg ((x \in B \land y \in D) \land z = F) \to (x \in B \land y \in D))$
107		tsan3	$⊢ \neg ((((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D)) \land (x \in A \to (y \in C \to (z = E \leftrightarrow z = F)))) \to (((x \in A \land y \in C) \land z = E) \leftrightarrow ((x \in B \land y \in D) \land z = F))) \to (y \in D \lor \neg (x \in B \land y \in D))$
108	107	a1d	$⊢ \neg ((((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D)) \land (x \in A \to (y \in C \to (z = E \leftrightarrow z = F)))) \to (((x \in A \land y \in C) \land z = E) \leftrightarrow ((x \in B \land y \in D) \land z = F))) \to (\neg \neg ((x \in B \land y \in D) \land z = F) \to (y \in D \lor \neg (x \in B \land y \in D)))$
109	106 108	cnfn2dd	$⊢ \neg ((((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D)) \land (x \in A \to (y \in C \to (z = E \leftrightarrow z = F)))) \to (((x \in A \land y \in C) \land z = E) \leftrightarrow ((x \in B \land y \in D) \land z = F))) \to (\neg \neg ((x \in B \land y \in D) \land z = F) \to y \in D)$
110		tsan3	$⊢ \neg ((((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D)) \land (x \in A \to (y \in C \to (z = E \leftrightarrow z = F)))) \to (((x \in A \land y \in C) \land z = E) \leftrightarrow ((x \in B \land y \in D) \land z = F))) \to ((y \in C \leftrightarrow y \in D) \lor \neg ((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D)))$
111	110	ord	$⊢ \neg ((((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D)) \land (x \in A \to (y \in C \to (z = E \leftrightarrow z = F)))) \to (((x \in A \land y \in C) \land z = E) \leftrightarrow ((x \in B \land y \in D) \land z = F))) \to (\neg (y \in C \leftrightarrow y \in D) \to \neg ((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D)))$
112	75	a1d	$⊢ \neg ((((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D)) \land (x \in A \to (y \in C \to (z = E \leftrightarrow z = F)))) \to (((x \in A \land y \in C) \land z = E) \leftrightarrow ((x \in B \land y \in D) \land z = F))) \to (\neg (y \in C \leftrightarrow y \in D) \to (((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D)) \lor \neg (((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D)) \land (x \in A \to (y \in C \to (z = E \leftrightarrow z = F))))))$
113	111 112	cnf1dd	$⊢ \neg ((((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D)) \land (x \in A \to (y \in C \to (z = E \leftrightarrow z = F)))) \to (((x \in A \land y \in C) \land z = E) \leftrightarrow ((x \in B \land y \in D) \land z = F))) \to (\neg (y \in C \leftrightarrow y \in D) \to \neg (((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D)) \land (x \in A \to (y \in C \to (z = E \leftrightarrow z = F)))))$
114	78	a1d	$⊢ \neg ((((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D)) \land (x \in A \to (y \in C \to (z = E \leftrightarrow z = F)))) \to (((x \in A \land y \in C) \land z = E) \leftrightarrow ((x \in B \land y \in D) \land z = F))) \to (\neg (y \in C \leftrightarrow y \in D) \to ((((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D)) \land (x \in A \to (y \in C \to (z = E \leftrightarrow z = F)))) \lor ((((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D)) \land (x \in A \to (y \in C \to (z = E \leftrightarrow z = F)))) \to (((x \in A \land y \in C) \land z = E) \leftrightarrow ((x \in B \land y \in D) \land z = F)))))$
115	113 114	cnf1dd	$⊢ \neg ((((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D)) \land (x \in A \to (y \in C \to (z = E \leftrightarrow z = F)))) \to (((x \in A \land y \in C) \land z = E) \leftrightarrow ((x \in B \land y \in D) \land z = F))) \to (\neg (y \in C \leftrightarrow y \in D) \to ((((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D)) \land (x \in A \to (y \in C \to (z = E \leftrightarrow z = F)))) \to (((x \in A \land y \in C) \land z = E) \leftrightarrow ((x \in B \land y \in D) \land z = F))))$
116		ax-1	$⊢ \neg ((((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D)) \land (x \in A \to (y \in C \to (z = E \leftrightarrow z = F)))) \to (((x \in A \land y \in C) \land z = E) \leftrightarrow ((x \in B \land y \in D) \land z = F))) \to (\neg (y \in C \leftrightarrow y \in D) \to \neg ((((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D)) \land (x \in A \to (y \in C \to (z = E \leftrightarrow z = F)))) \to (((x \in A \land y \in C) \land z = E) \leftrightarrow ((x \in B \land y \in D) \land z = F))))$
117	115 116	contrd	$⊢ \neg ((((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D)) \land (x \in A \to (y \in C \to (z = E \leftrightarrow z = F)))) \to (((x \in A \land y \in C) \land z = E) \leftrightarrow ((x \in B \land y \in D) \land z = F))) \to (y \in C \leftrightarrow y \in D)$
118	109 117	sylibrd	$⊢ \neg ((((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D)) \land (x \in A \to (y \in C \to (z = E \leftrightarrow z = F)))) \to (((x \in A \land y \in C) \land z = E) \leftrightarrow ((x \in B \land y \in D) \land z = F))) \to (\neg \neg ((x \in B \land y \in D) \land z = F) \to y \in C)$
119	94	a1d	$⊢ \neg ((((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D)) \land (x \in A \to (y \in C \to (z = E \leftrightarrow z = F)))) \to (((x \in A \land y \in C) \land z = E) \leftrightarrow ((x \in B \land y \in D) \land z = F))) \to (\neg \neg ((x \in B \land y \in D) \land z = F) \to x \in A)$
120		ax-1	$⊢ \neg ((((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D)) \land (x \in A \to (y \in C \to (z = E \leftrightarrow z = F)))) \to (((x \in A \land y \in C) \land z = E) \leftrightarrow ((x \in B \land y \in D) \land z = F))) \to (\neg \neg ((x \in B \land y \in D) \land z = F) \to \neg ((((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D)) \land (x \in A \to (y \in C \to (z = E \leftrightarrow z = F)))) \to (((x \in A \land y \in C) \land z = E) \leftrightarrow ((x \in B \land y \in D) \land z = F))))$
121	78	a1d	$⊢ \neg ((((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D)) \land (x \in A \to (y \in C \to (z = E \leftrightarrow z = F)))) \to (((x \in A \land y \in C) \land z = E) \leftrightarrow ((x \in B \land y \in D) \land z = F))) \to (\neg \neg ((x \in B \land y \in D) \land z = F) \to ((((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D)) \land (x \in A \to (y \in C \to (z = E \leftrightarrow z = F)))) \lor ((((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D)) \land (x \in A \to (y \in C \to (z = E \leftrightarrow z = F)))) \to (((x \in A \land y \in C) \land z = E) \leftrightarrow ((x \in B \land y \in D) \land z = F)))))$
122	120 121	cnf2dd	$⊢ \neg ((((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D)) \land (x \in A \to (y \in C \to (z = E \leftrightarrow z = F)))) \to (((x \in A \land y \in C) \land z = E) \leftrightarrow ((x \in B \land y \in D) \land z = F))) \to (\neg \neg ((x \in B \land y \in D) \land z = F) \to (((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D)) \land (x \in A \to (y \in C \to (z = E \leftrightarrow z = F)))))$
123	99	a1d	$⊢ \neg ((((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D)) \land (x \in A \to (y \in C \to (z = E \leftrightarrow z = F)))) \to (((x \in A \land y \in C) \land z = E) \leftrightarrow ((x \in B \land y \in D) \land z = F))) \to (\neg \neg ((x \in B \land y \in D) \land z = F) \to ((x \in A \to (y \in C \to (z = E \leftrightarrow z = F))) \lor \neg (((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D)) \land (x \in A \to (y \in C \to (z = E \leftrightarrow z = F))))))$
124	122 123	cnfn2dd	$⊢ \neg ((((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D)) \land (x \in A \to (y \in C \to (z = E \leftrightarrow z = F)))) \to (((x \in A \land y \in C) \land z = E) \leftrightarrow ((x \in B \land y \in D) \land z = F))) \to (\neg \neg ((x \in B \land y \in D) \land z = F) \to (x \in A \to (y \in C \to (z = E \leftrightarrow z = F))))$
125	119 124	mpdd	$⊢ \neg ((((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D)) \land (x \in A \to (y \in C \to (z = E \leftrightarrow z = F)))) \to (((x \in A \land y \in C) \land z = E) \leftrightarrow ((x \in B \land y \in D) \land z = F))) \to (\neg \neg ((x \in B \land y \in D) \land z = F) \to (y \in C \to (z = E \leftrightarrow z = F)))$
126	118 125	mpdd	$⊢ \neg ((((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D)) \land (x \in A \to (y \in C \to (z = E \leftrightarrow z = F)))) \to (((x \in A \land y \in C) \land z = E) \leftrightarrow ((x \in B \land y \in D) \land z = F))) \to (\neg \neg ((x \in B \land y \in D) \land z = F) \to (z = E \leftrightarrow z = F))$
127	119 118	jcad	$⊢ \neg ((((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D)) \land (x \in A \to (y \in C \to (z = E \leftrightarrow z = F)))) \to (((x \in A \land y \in C) \land z = E) \leftrightarrow ((x \in B \land y \in D) \land z = F))) \to (\neg \neg ((x \in B \land y \in D) \land z = F) \to (x \in A \land y \in C))$
128		tsim3	$⊢ \neg ((((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D)) \land (x \in A \to (y \in C \to (z = E \leftrightarrow z = F)))) \to (((x \in A \land y \in C) \land z = E) \leftrightarrow ((x \in B \land y \in D) \land z = F))) \to (\neg (((x \in A \land y \in C) \land z = E) \leftrightarrow ((x \in B \land y \in D) \land z = F)) \lor ((((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D)) \land (x \in A \to (y \in C \to (z = E \leftrightarrow z = F)))) \to (((x \in A \land y \in C) \land z = E) \leftrightarrow ((x \in B \land y \in D) \land z = F))))$
129	128	a1d	$⊢ \neg ((((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D)) \land (x \in A \to (y \in C \to (z = E \leftrightarrow z = F)))) \to (((x \in A \land y \in C) \land z = E) \leftrightarrow ((x \in B \land y \in D) \land z = F))) \to (\neg \neg ((x \in B \land y \in D) \land z = F) \to (\neg (((x \in A \land y \in C) \land z = E) \leftrightarrow ((x \in B \land y \in D) \land z = F)) \lor ((((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D)) \land (x \in A \to (y \in C \to (z = E \leftrightarrow z = F)))) \to (((x \in A \land y \in C) \land z = E) \leftrightarrow ((x \in B \land y \in D) \land z = F)))))$
130	120 129	cnf2dd	$⊢ \neg ((((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D)) \land (x \in A \to (y \in C \to (z = E \leftrightarrow z = F)))) \to (((x \in A \land y \in C) \land z = E) \leftrightarrow ((x \in B \land y \in D) \land z = F))) \to (\neg \neg ((x \in B \land y \in D) \land z = F) \to \neg (((x \in A \land y \in C) \land z = E) \leftrightarrow ((x \in B \land y \in D) \land z = F)))$
131		tsbi1	$⊢ \neg ((((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D)) \land (x \in A \to (y \in C \to (z = E \leftrightarrow z = F)))) \to (((x \in A \land y \in C) \land z = E) \leftrightarrow ((x \in B \land y \in D) \land z = F))) \to ((\neg ((x \in A \land y \in C) \land z = E) \lor \neg ((x \in B \land y \in D) \land z = F)) \lor (((x \in A \land y \in C) \land z = E) \leftrightarrow ((x \in B \land y \in D) \land z = F)))$
132	131	a1d	$⊢ \neg ((((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D)) \land (x \in A \to (y \in C \to (z = E \leftrightarrow z = F)))) \to (((x \in A \land y \in C) \land z = E) \leftrightarrow ((x \in B \land y \in D) \land z = F))) \to (\neg \neg ((x \in B \land y \in D) \land z = F) \to ((\neg ((x \in A \land y \in C) \land z = E) \lor \neg ((x \in B \land y \in D) \land z = F)) \lor (((x \in A \land y \in C) \land z = E) \leftrightarrow ((x \in B \land y \in D) \land z = F))))$
133	130 132	cnf2dd	$⊢ \neg ((((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D)) \land (x \in A \to (y \in C \to (z = E \leftrightarrow z = F)))) \to (((x \in A \land y \in C) \land z = E) \leftrightarrow ((x \in B \land y \in D) \land z = F))) \to (\neg \neg ((x \in B \land y \in D) \land z = F) \to (\neg ((x \in A \land y \in C) \land z = E) \lor \neg ((x \in B \land y \in D) \land z = F)))$
134	104 133	cnfn2dd	$⊢ \neg ((((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D)) \land (x \in A \to (y \in C \to (z = E \leftrightarrow z = F)))) \to (((x \in A \land y \in C) \land z = E) \leftrightarrow ((x \in B \land y \in D) \land z = F))) \to (\neg \neg ((x \in B \land y \in D) \land z = F) \to \neg ((x \in A \land y \in C) \land z = E))$
135		tsan1	$⊢ \neg ((((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D)) \land (x \in A \to (y \in C \to (z = E \leftrightarrow z = F)))) \to (((x \in A \land y \in C) \land z = E) \leftrightarrow ((x \in B \land y \in D) \land z = F))) \to ((\neg (x \in A \land y \in C) \lor \neg z = E) \lor ((x \in A \land y \in C) \land z = E))$
136	135	a1d	$⊢ \neg ((((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D)) \land (x \in A \to (y \in C \to (z = E \leftrightarrow z = F)))) \to (((x \in A \land y \in C) \land z = E) \leftrightarrow ((x \in B \land y \in D) \land z = F))) \to (\neg \neg ((x \in B \land y \in D) \land z = F) \to ((\neg (x \in A \land y \in C) \lor \neg z = E) \lor ((x \in A \land y \in C) \land z = E)))$
137	134 136	cnf2dd	$⊢ \neg ((((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D)) \land (x \in A \to (y \in C \to (z = E \leftrightarrow z = F)))) \to (((x \in A \land y \in C) \land z = E) \leftrightarrow ((x \in B \land y \in D) \land z = F))) \to (\neg \neg ((x \in B \land y \in D) \land z = F) \to (\neg (x \in A \land y \in C) \lor \neg z = E))$
138	127 137	cnfn1dd	$⊢ \neg ((((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D)) \land (x \in A \to (y \in C \to (z = E \leftrightarrow z = F)))) \to (((x \in A \land y \in C) \land z = E) \leftrightarrow ((x \in B \land y \in D) \land z = F))) \to (\neg \neg ((x \in B \land y \in D) \land z = F) \to \neg z = E)$
139		tsan3	$⊢ \neg ((((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D)) \land (x \in A \to (y \in C \to (z = E \leftrightarrow z = F)))) \to (((x \in A \land y \in C) \land z = E) \leftrightarrow ((x \in B \land y \in D) \land z = F))) \to (z = F \lor \neg ((x \in B \land y \in D) \land z = F))$
140	139	a1d	$⊢ \neg ((((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D)) \land (x \in A \to (y \in C \to (z = E \leftrightarrow z = F)))) \to (((x \in A \land y \in C) \land z = E) \leftrightarrow ((x \in B \land y \in D) \land z = F))) \to (\neg \neg ((x \in B \land y \in D) \land z = F) \to (z = F \lor \neg ((x \in B \land y \in D) \land z = F)))$
141	104 140	cnfn2dd	$⊢ \neg ((((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D)) \land (x \in A \to (y \in C \to (z = E \leftrightarrow z = F)))) \to (((x \in A \land y \in C) \land z = E) \leftrightarrow ((x \in B \land y \in D) \land z = F))) \to (\neg \neg ((x \in B \land y \in D) \land z = F) \to z = F)$
142		tsbi3	$⊢ \neg ((((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D)) \land (x \in A \to (y \in C \to (z = E \leftrightarrow z = F)))) \to (((x \in A \land y \in C) \land z = E) \leftrightarrow ((x \in B \land y \in D) \land z = F))) \to ((z = E \lor \neg z = F) \lor \neg (z = E \leftrightarrow z = F))$
143	142	a1d	$⊢ \neg ((((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D)) \land (x \in A \to (y \in C \to (z = E \leftrightarrow z = F)))) \to (((x \in A \land y \in C) \land z = E) \leftrightarrow ((x \in B \land y \in D) \land z = F))) \to (\neg \neg ((x \in B \land y \in D) \land z = F) \to ((z = E \lor \neg z = F) \lor \neg (z = E \leftrightarrow z = F)))$
144	143	or32dd	$⊢ \neg ((((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D)) \land (x \in A \to (y \in C \to (z = E \leftrightarrow z = F)))) \to (((x \in A \land y \in C) \land z = E) \leftrightarrow ((x \in B \land y \in D) \land z = F))) \to (\neg \neg ((x \in B \land y \in D) \land z = F) \to ((z = E \lor \neg (z = E \leftrightarrow z = F)) \lor \neg z = F))$
145	141 144	cnfn2dd	$⊢ \neg ((((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D)) \land (x \in A \to (y \in C \to (z = E \leftrightarrow z = F)))) \to (((x \in A \land y \in C) \land z = E) \leftrightarrow ((x \in B \land y \in D) \land z = F))) \to (\neg \neg ((x \in B \land y \in D) \land z = F) \to (z = E \lor \neg (z = E \leftrightarrow z = F)))$
146	138 145	cnf1dd	$⊢ \neg ((((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D)) \land (x \in A \to (y \in C \to (z = E \leftrightarrow z = F)))) \to (((x \in A \land y \in C) \land z = E) \leftrightarrow ((x \in B \land y \in D) \land z = F))) \to (\neg \neg ((x \in B \land y \in D) \land z = F) \to \neg (z = E \leftrightarrow z = F))$
147	126 146	contrd	$⊢ \neg ((((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D)) \land (x \in A \to (y \in C \to (z = E \leftrightarrow z = F)))) \to (((x \in A \land y \in C) \land z = E) \leftrightarrow ((x \in B \land y \in D) \land z = F))) \to \neg ((x \in B \land y \in D) \land z = F)$
148	147	a1d	$⊢ \neg ((((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D)) \land (x \in A \to (y \in C \to (z = E \leftrightarrow z = F)))) \to (((x \in A \land y \in C) \land z = E) \leftrightarrow ((x \in B \land y \in D) \land z = F))) \to (\neg ⊥ \to \neg ((x \in B \land y \in D) \land z = F))$
149	128	a1d	$⊢ \neg ((((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D)) \land (x \in A \to (y \in C \to (z = E \leftrightarrow z = F)))) \to (((x \in A \land y \in C) \land z = E) \leftrightarrow ((x \in B \land y \in D) \land z = F))) \to (\neg ⊥ \to (\neg (((x \in A \land y \in C) \land z = E) \leftrightarrow ((x \in B \land y \in D) \land z = F)) \lor ((((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D)) \land (x \in A \to (y \in C \to (z = E \leftrightarrow z = F)))) \to (((x \in A \land y \in C) \land z = E) \leftrightarrow ((x \in B \land y \in D) \land z = F)))))$
150	96 149	cnf2dd	$⊢ \neg ((((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D)) \land (x \in A \to (y \in C \to (z = E \leftrightarrow z = F)))) \to (((x \in A \land y \in C) \land z = E) \leftrightarrow ((x \in B \land y \in D) \land z = F))) \to (\neg ⊥ \to \neg (((x \in A \land y \in C) \land z = E) \leftrightarrow ((x \in B \land y \in D) \land z = F)))$
151	65	a1d	$⊢ \neg ((((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D)) \land (x \in A \to (y \in C \to (z = E \leftrightarrow z = F)))) \to (((x \in A \land y \in C) \land z = E) \leftrightarrow ((x \in B \land y \in D) \land z = F))) \to (\neg ⊥ \to ((((x \in A \land y \in C) \land z = E) \lor ((x \in B \land y \in D) \land z = F)) \lor (((x \in A \land y \in C) \land z = E) \leftrightarrow ((x \in B \land y \in D) \land z = F))))$
152	150 151	cnf2dd	$⊢ \neg ((((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D)) \land (x \in A \to (y \in C \to (z = E \leftrightarrow z = F)))) \to (((x \in A \land y \in C) \land z = E) \leftrightarrow ((x \in B \land y \in D) \land z = F))) \to (\neg ⊥ \to (((x \in A \land y \in C) \land z = E) \lor ((x \in B \land y \in D) \land z = F)))$
153	148 152	cnf2dd	$⊢ \neg ((((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D)) \land (x \in A \to (y \in C \to (z = E \leftrightarrow z = F)))) \to (((x \in A \land y \in C) \land z = E) \leftrightarrow ((x \in B \land y \in D) \land z = F))) \to (\neg ⊥ \to ((x \in A \land y \in C) \land z = E))$
154	62	a1d	$⊢ \neg ((((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D)) \land (x \in A \to (y \in C \to (z = E \leftrightarrow z = F)))) \to (((x \in A \land y \in C) \land z = E) \leftrightarrow ((x \in B \land y \in D) \land z = F))) \to (\neg ⊥ \to ((x \in A \land y \in C) \lor \neg ((x \in A \land y \in C) \land z = E)))$
155	153 154	cnfn2dd	$⊢ \neg ((((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D)) \land (x \in A \to (y \in C \to (z = E \leftrightarrow z = F)))) \to (((x \in A \land y \in C) \land z = E) \leftrightarrow ((x \in B \land y \in D) \land z = F))) \to (\neg ⊥ \to (x \in A \land y \in C))$
156		tsan3	$⊢ \neg ((((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D)) \land (x \in A \to (y \in C \to (z = E \leftrightarrow z = F)))) \to (((x \in A \land y \in C) \land z = E) \leftrightarrow ((x \in B \land y \in D) \land z = F))) \to (y \in C \lor \neg (x \in A \land y \in C))$
157	156	a1d	$⊢ \neg ((((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D)) \land (x \in A \to (y \in C \to (z = E \leftrightarrow z = F)))) \to (((x \in A \land y \in C) \land z = E) \leftrightarrow ((x \in B \land y \in D) \land z = F))) \to (\neg ⊥ \to (y \in C \lor \neg (x \in A \land y \in C)))$
158	155 157	cnfn2dd	$⊢ \neg ((((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D)) \land (x \in A \to (y \in C \to (z = E \leftrightarrow z = F)))) \to (((x \in A \land y \in C) \land z = E) \leftrightarrow ((x \in B \land y \in D) \land z = F))) \to (\neg ⊥ \to y \in C)$
159		tsan3	$⊢ \neg ((((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D)) \land (x \in A \to (y \in C \to (z = E \leftrightarrow z = F)))) \to (((x \in A \land y \in C) \land z = E) \leftrightarrow ((x \in B \land y \in D) \land z = F))) \to (z = E \lor \neg ((x \in A \land y \in C) \land z = E))$
160	159	a1d	$⊢ \neg ((((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D)) \land (x \in A \to (y \in C \to (z = E \leftrightarrow z = F)))) \to (((x \in A \land y \in C) \land z = E) \leftrightarrow ((x \in B \land y \in D) \land z = F))) \to (\neg ⊥ \to (z = E \lor \neg ((x \in A \land y \in C) \land z = E)))$
161	153 160	cnfn2dd	$⊢ \neg ((((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D)) \land (x \in A \to (y \in C \to (z = E \leftrightarrow z = F)))) \to (((x \in A \land y \in C) \land z = E) \leftrightarrow ((x \in B \land y \in D) \land z = F))) \to (\neg ⊥ \to z = E)$
162	95 82	sylibd	$⊢ \neg ((((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D)) \land (x \in A \to (y \in C \to (z = E \leftrightarrow z = F)))) \to (((x \in A \land y \in C) \land z = E) \leftrightarrow ((x \in B \land y \in D) \land z = F))) \to (\neg ⊥ \to x \in B)$
163	158 117	sylibd	$⊢ \neg ((((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D)) \land (x \in A \to (y \in C \to (z = E \leftrightarrow z = F)))) \to (((x \in A \land y \in C) \land z = E) \leftrightarrow ((x \in B \land y \in D) \land z = F))) \to (\neg ⊥ \to y \in D)$
164	162 163	jcad	$⊢ \neg ((((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D)) \land (x \in A \to (y \in C \to (z = E \leftrightarrow z = F)))) \to (((x \in A \land y \in C) \land z = E) \leftrightarrow ((x \in B \land y \in D) \land z = F))) \to (\neg ⊥ \to (x \in B \land y \in D))$
165		tsan1	$⊢ \neg ((((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D)) \land (x \in A \to (y \in C \to (z = E \leftrightarrow z = F)))) \to (((x \in A \land y \in C) \land z = E) \leftrightarrow ((x \in B \land y \in D) \land z = F))) \to ((\neg (x \in B \land y \in D) \lor \neg z = F) \lor ((x \in B \land y \in D) \land z = F))$
166	165	a1d	$⊢ \neg ((((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D)) \land (x \in A \to (y \in C \to (z = E \leftrightarrow z = F)))) \to (((x \in A \land y \in C) \land z = E) \leftrightarrow ((x \in B \land y \in D) \land z = F))) \to (\neg ⊥ \to ((\neg (x \in B \land y \in D) \lor \neg z = F) \lor ((x \in B \land y \in D) \land z = F)))$
167	148 166	cnf2dd	$⊢ \neg ((((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D)) \land (x \in A \to (y \in C \to (z = E \leftrightarrow z = F)))) \to (((x \in A \land y \in C) \land z = E) \leftrightarrow ((x \in B \land y \in D) \land z = F))) \to (\neg ⊥ \to (\neg (x \in B \land y \in D) \lor \neg z = F))$
168	164 167	cnfn1dd	$⊢ \neg ((((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D)) \land (x \in A \to (y \in C \to (z = E \leftrightarrow z = F)))) \to (((x \in A \land y \in C) \land z = E) \leftrightarrow ((x \in B \land y \in D) \land z = F))) \to (\neg ⊥ \to \neg z = F)$
169		tsbi4	$⊢ \neg ((((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D)) \land (x \in A \to (y \in C \to (z = E \leftrightarrow z = F)))) \to (((x \in A \land y \in C) \land z = E) \leftrightarrow ((x \in B \land y \in D) \land z = F))) \to ((\neg z = E \lor z = F) \lor \neg (z = E \leftrightarrow z = F))$
170	169	a1d	$⊢ \neg ((((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D)) \land (x \in A \to (y \in C \to (z = E \leftrightarrow z = F)))) \to (((x \in A \land y \in C) \land z = E) \leftrightarrow ((x \in B \land y \in D) \land z = F))) \to (\neg ⊥ \to ((\neg z = E \lor z = F) \lor \neg (z = E \leftrightarrow z = F)))$
171	170	or32dd	$⊢ \neg ((((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D)) \land (x \in A \to (y \in C \to (z = E \leftrightarrow z = F)))) \to (((x \in A \land y \in C) \land z = E) \leftrightarrow ((x \in B \land y \in D) \land z = F))) \to (\neg ⊥ \to ((\neg z = E \lor \neg (z = E \leftrightarrow z = F)) \lor z = F))$
172	168 171	cnf2dd	$⊢ \neg ((((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D)) \land (x \in A \to (y \in C \to (z = E \leftrightarrow z = F)))) \to (((x \in A \land y \in C) \land z = E) \leftrightarrow ((x \in B \land y \in D) \land z = F))) \to (\neg ⊥ \to (\neg z = E \lor \neg (z = E \leftrightarrow z = F)))$
173	161 172	cnfn1dd	$⊢ \neg ((((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D)) \land (x \in A \to (y \in C \to (z = E \leftrightarrow z = F)))) \to (((x \in A \land y \in C) \land z = E) \leftrightarrow ((x \in B \land y \in D) \land z = F))) \to (\neg ⊥ \to \neg (z = E \leftrightarrow z = F))$
174		tsim1	$⊢ \neg ((((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D)) \land (x \in A \to (y \in C \to (z = E \leftrightarrow z = F)))) \to (((x \in A \land y \in C) \land z = E) \leftrightarrow ((x \in B \land y \in D) \land z = F))) \to ((\neg y \in C \lor (z = E \leftrightarrow z = F)) \lor \neg (y \in C \to (z = E \leftrightarrow z = F)))$
175	174	a1d	$⊢ \neg ((((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D)) \land (x \in A \to (y \in C \to (z = E \leftrightarrow z = F)))) \to (((x \in A \land y \in C) \land z = E) \leftrightarrow ((x \in B \land y \in D) \land z = F))) \to (\neg ⊥ \to ((\neg y \in C \lor (z = E \leftrightarrow z = F)) \lor \neg (y \in C \to (z = E \leftrightarrow z = F))))$
176	175	or32dd	$⊢ \neg ((((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D)) \land (x \in A \to (y \in C \to (z = E \leftrightarrow z = F)))) \to (((x \in A \land y \in C) \land z = E) \leftrightarrow ((x \in B \land y \in D) \land z = F))) \to (\neg ⊥ \to ((\neg y \in C \lor \neg (y \in C \to (z = E \leftrightarrow z = F))) \lor (z = E \leftrightarrow z = F)))$
177	173 176	cnf2dd	$⊢ \neg ((((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D)) \land (x \in A \to (y \in C \to (z = E \leftrightarrow z = F)))) \to (((x \in A \land y \in C) \land z = E) \leftrightarrow ((x \in B \land y \in D) \land z = F))) \to (\neg ⊥ \to (\neg y \in C \lor \neg (y \in C \to (z = E \leftrightarrow z = F))))$
178	158 177	cnfn1dd	$⊢ \neg ((((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D)) \land (x \in A \to (y \in C \to (z = E \leftrightarrow z = F)))) \to (((x \in A \land y \in C) \land z = E) \leftrightarrow ((x \in B \land y \in D) \land z = F))) \to (\neg ⊥ \to \neg (y \in C \to (z = E \leftrightarrow z = F)))$
179	102 178	contrd	$⊢ \neg ((((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D)) \land (x \in A \to (y \in C \to (z = E \leftrightarrow z = F)))) \to (((x \in A \land y \in C) \land z = E) \leftrightarrow ((x \in B \land y \in D) \land z = F))) \to ⊥$
180	179	efald2	$⊢ (((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D)) \land (x \in A \to (y \in C \to (z = E \leftrightarrow z = F)))) \to (((x \in A \land y \in C) \land z = E) \leftrightarrow ((x \in B \land y \in D) \land z = F))$
181	180	alimi	$⊢ \forall z (((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D)) \land (x \in A \to (y \in C \to (z = E \leftrightarrow z = F)))) \to \forall z (((x \in A \land y \in C) \land z = E) \leftrightarrow ((x \in B \land y \in D) \land z = F))$
182	181	2alimi	$⊢ \forall x \forall y \forall z (((x \in A \leftrightarrow x \in B) \land (y \in C \leftrightarrow y \in D)) \land (x \in A \to (y \in C \to (z = E \leftrightarrow z = F)))) \to \forall x \forall y \forall z (((x \in A \land y \in C) \land z = E) \leftrightarrow ((x \in B \land y \in D) \land z = F))$
183		oprabbi	$⊢ \forall x \forall y \forall z (((x \in A \land y \in C) \land z = E) \leftrightarrow ((x \in B \land y \in D) \land z = F)) \to \{⟨⟨x, y⟩, z⟩ \| ((x \in A \land y \in C) \land z = E)\} = \{⟨⟨x, y⟩, z⟩ \| ((x \in B \land y \in D) \land z = F)\}$
184	59 182 183	3syl	$⊢ ((A = B \land C = D) \land \forall x \in A \forall y \in C E = F) \to \{⟨⟨x, y⟩, z⟩ \| ((x \in A \land y \in C) \land z = E)\} = \{⟨⟨x, y⟩, z⟩ \| ((x \in B \land y \in D) \land z = F)\}$
185		df-mpo	$⊢ (x \in A, y \in C ⟼ E) = \{⟨⟨x, y⟩, z⟩ \| ((x \in A \land y \in C) \land z = E)\}$
186		df-mpo	$⊢ (x \in B, y \in D ⟼ F) = \{⟨⟨x, y⟩, z⟩ \| ((x \in B \land y \in D) \land z = F)\}$
187	184 185 186	3eqtr4g	$⊢ ((A = B \land C = D) \land \forall x \in A \forall y \in C E = F) \to (x \in A, y \in C ⟼ E) = (x \in B, y \in D ⟼ F)$

Metamath Proof Explorer

Theorem mpobi123f

Proof