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	37 44 47 52	4syl	$⊢ \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)))$
54		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))))$
55	54	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))))$
56	55	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))))$
57	56	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))))$
58	34 53 57	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))))$
59		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))$
60	59	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))$
61		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))$
62	61	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)))$
63	60 62	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))$
64		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)))$
65	64	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)))$
66	65	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))))$
67		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))))$
68	66 67	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))$
69	68	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)))$
70	63 69	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))$
71		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)$
72		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)))$
73	72	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)))$
74		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)))))$
75	74	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))))))$
76	73 75	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)))))$
77		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))))$
78	77	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)))))$
79	76 78	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))))$
80		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))))$
81	79 80	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)$
82	81	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))$
83		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))$
84	83	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)))$
85	82 84	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))$
86	71 85	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)$
87		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))$
88	87	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)))$
89	86 88	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))$
90		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))$
91	90	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)))$
92	89 91	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))$
93	70 92	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$
94	93	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)$
95		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))))$
96	77	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)))))$
97	95 96	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)))))$
98		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)))))$
99	98	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))))))$
100	97 99	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))))$
101	94 100	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)))$
102		notnotr	$⊢ \neg \neg ((x \in B \land y \in D) \land z = F) \to ((x \in B \land y \in D) \land z = F)$
103	102	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))$
104	90	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)))$
105	103 104	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))$
106		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))$
107	106	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)))$
108	105 107	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)$
109		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)))$
110	109	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)))$
111	74	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))))))$
112	110 111	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)))))$
113	77	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)))))$
114	112 113	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))))$
115		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))))$
116	114 115	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)$
117	108 116	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)$
118	93	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)$
119		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))))$
120	77	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)))))$
121	119 120	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)))))$
122	98	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))))))$
123	121 122	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))))$
124	118 123	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)))$
125	117 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 (z = E \leftrightarrow z = F))$
126	118 117	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))$
127		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))))$
128	127	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)))))$
129	119 128	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)))$
130		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)))$
131	130	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))))$
132	129 131	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)))$
133	103 132	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))$
134		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))$
135	134	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)))$
136	133 135	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))$
137	126 136	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)$
138		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))$
139	138	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)))$
140	103 139	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)$
141		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))$
142	141	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)))$
143	142	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))$
144	140 143	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)))$
145	137 144	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))$
146	125 145	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)$
147	146	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))$
148	127	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)))))$
149	95 148	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)))$
150	64	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))))$
151	149 150	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)))$
152	147 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))$
153	61	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)))$
154	152 153	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))$
155		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))$
156	155	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)))$
157	154 156	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)$
158		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))$
159	158	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)))$
160	152 159	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)$
161	94 81	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)$
162	157 116	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)$
163	161 162	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))$
164		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))$
165	164	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)))$
166	147 165	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))$
167	163 166	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)$
168		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))$
169	168	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)))$
170	169	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))$
171	167 170	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)))$
172	160 171	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))$
173		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)))$
174	173	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))))$
175	174	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)))$
176	172 175	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))))$
177	157 176	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)))$
178	101 177	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 ⊥$
179	178	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))$
180	179	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))$
181	180	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))$
182		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)\}$
183	58 181 182	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)\}$
184		df-mpo	$⊢ (x \in A, y \in C ⟼ E) = \{⟨⟨x, y⟩, z⟩ \| ((x \in A \land y \in C) \land z = E)\}$
185		df-mpo	$⊢ (x \in B, y \in D ⟼ F) = \{⟨⟨x, y⟩, z⟩ \| ((x \in B \land y \in D) \land z = F)\}$
186	183 184 185	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