mptbi12f

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

	Ref	Expression
Hypotheses	mptbi12f.1	$⊢ \underline{Ⅎ} x A$
	mptbi12f.2	$⊢ \underline{Ⅎ} x B$
Assertion	mptbi12f	$⊢ (A = B \land \forall x \in A D = E) \to (x \in A ⟼ D) = (x \in B ⟼ E)$

Proof

Step	Hyp	Ref	Expression
1		mptbi12f.1	$⊢ \underline{Ⅎ} x A$
2		mptbi12f.2	$⊢ \underline{Ⅎ} x B$
3	1 2	nfeq	$⊢ Ⅎ x A = B$
4		eleq2	$⊢ A = B \to (x \in A \leftrightarrow x \in B)$
5	3 4	alrimi	$⊢ A = B \to \forall x (x \in A \leftrightarrow x \in B)$
6		ax-5	$⊢ (x \in A \leftrightarrow x \in B) \to \forall y (x \in A \leftrightarrow x \in B)$
7	5 6	sylg	$⊢ A = B \to \forall x \forall y (x \in A \leftrightarrow x \in B)$
8		eqeq2	$⊢ D = E \to (y = D \leftrightarrow y = E)$
9	8	alrimiv	$⊢ D = E \to \forall y (y = D \leftrightarrow y = E)$
10	9	ralimi	$⊢ \forall x \in A D = E \to \forall x \in A \forall y (y = D \leftrightarrow y = E)$
11		df-ral	$⊢ \forall x \in A \forall y (y = D \leftrightarrow y = E) \leftrightarrow \forall x (x \in A \to \forall y (y = D \leftrightarrow y = E))$
12	10 11	sylib	$⊢ \forall x \in A D = E \to \forall x (x \in A \to \forall y (y = D \leftrightarrow y = E))$
13		19.21v	$⊢ \forall y (x \in A \to (y = D \leftrightarrow y = E)) \leftrightarrow (x \in A \to \forall y (y = D \leftrightarrow y = E))$
14	13	albii	$⊢ \forall x \forall y (x \in A \to (y = D \leftrightarrow y = E)) \leftrightarrow \forall x (x \in A \to \forall y (y = D \leftrightarrow y = E))$
15	12 14	sylibr	$⊢ \forall x \in A D = E \to \forall x \forall y (x \in A \to (y = D \leftrightarrow y = E))$
16		id	$⊢ ((x \in A \leftrightarrow x \in B) \land (x \in A \to (y = D \leftrightarrow y = E))) \to ((x \in A \leftrightarrow x \in B) \land (x \in A \to (y = D \leftrightarrow y = E)))$
17	16	alanimi	$⊢ (\forall y (x \in A \leftrightarrow x \in B) \land \forall y (x \in A \to (y = D \leftrightarrow y = E))) \to \forall y ((x \in A \leftrightarrow x \in B) \land (x \in A \to (y = D \leftrightarrow y = E)))$
18	17	alanimi	$⊢ (\forall x \forall y (x \in A \leftrightarrow x \in B) \land \forall x \forall y (x \in A \to (y = D \leftrightarrow y = E))) \to \forall x \forall y ((x \in A \leftrightarrow x \in B) \land (x \in A \to (y = D \leftrightarrow y = E)))$
19	7 15 18	syl2an	$⊢ (A = B \land \forall x \in A D = E) \to \forall x \forall y ((x \in A \leftrightarrow x \in B) \land (x \in A \to (y = D \leftrightarrow y = E)))$
20		tsan2	$⊢ \neg (((x \in A \leftrightarrow x \in B) \land (x \in A \to (y = D \leftrightarrow y = E))) \to ((x \in A \land y = D) \leftrightarrow (x \in B \land y = E))) \to (x \in A \lor \neg (x \in A \land y = D))$
21	20	ord	$⊢ \neg (((x \in A \leftrightarrow x \in B) \land (x \in A \to (y = D \leftrightarrow y = E))) \to ((x \in A \land y = D) \leftrightarrow (x \in B \land y = E))) \to (\neg x \in A \to \neg (x \in A \land y = D))$
22		tsbi2	$⊢ \neg (((x \in A \leftrightarrow x \in B) \land (x \in A \to (y = D \leftrightarrow y = E))) \to ((x \in A \land y = D) \leftrightarrow (x \in B \land y = E))) \to (((x \in A \land y = D) \lor (x \in B \land y = E)) \lor ((x \in A \land y = D) \leftrightarrow (x \in B \land y = E)))$
23	22	ord	$⊢ \neg (((x \in A \leftrightarrow x \in B) \land (x \in A \to (y = D \leftrightarrow y = E))) \to ((x \in A \land y = D) \leftrightarrow (x \in B \land y = E))) \to (\neg ((x \in A \land y = D) \lor (x \in B \land y = E)) \to ((x \in A \land y = D) \leftrightarrow (x \in B \land y = E)))$
24	23	a1dd	$⊢ \neg (((x \in A \leftrightarrow x \in B) \land (x \in A \to (y = D \leftrightarrow y = E))) \to ((x \in A \land y = D) \leftrightarrow (x \in B \land y = E))) \to (\neg ((x \in A \land y = D) \lor (x \in B \land y = E)) \to (((x \in A \leftrightarrow x \in B) \land (x \in A \to (y = D \leftrightarrow y = E))) \to ((x \in A \land y = D) \leftrightarrow (x \in B \land y = E))))$
25		ax-1	$⊢ \neg (((x \in A \leftrightarrow x \in B) \land (x \in A \to (y = D \leftrightarrow y = E))) \to ((x \in A \land y = D) \leftrightarrow (x \in B \land y = E))) \to (\neg ((x \in A \land y = D) \lor (x \in B \land y = E)) \to \neg (((x \in A \leftrightarrow x \in B) \land (x \in A \to (y = D \leftrightarrow y = E))) \to ((x \in A \land y = D) \leftrightarrow (x \in B \land y = E))))$
26	24 25	contrd	$⊢ \neg (((x \in A \leftrightarrow x \in B) \land (x \in A \to (y = D \leftrightarrow y = E))) \to ((x \in A \land y = D) \leftrightarrow (x \in B \land y = E))) \to ((x \in A \land y = D) \lor (x \in B \land y = E))$
27	26	a1d	$⊢ \neg (((x \in A \leftrightarrow x \in B) \land (x \in A \to (y = D \leftrightarrow y = E))) \to ((x \in A \land y = D) \leftrightarrow (x \in B \land y = E))) \to (\neg x \in A \to ((x \in A \land y = D) \lor (x \in B \land y = E)))$
28	21 27	cnf1dd	$⊢ \neg (((x \in A \leftrightarrow x \in B) \land (x \in A \to (y = D \leftrightarrow y = E))) \to ((x \in A \land y = D) \leftrightarrow (x \in B \land y = E))) \to (\neg x \in A \to (x \in B \land y = E))$
29		simplim	$⊢ \neg (((x \in A \leftrightarrow x \in B) \land (x \in A \to (y = D \leftrightarrow y = E))) \to ((x \in A \land y = D) \leftrightarrow (x \in B \land y = E))) \to ((x \in A \leftrightarrow x \in B) \land (x \in A \to (y = D \leftrightarrow y = E)))$
30	29	a1d	$⊢ \neg (((x \in A \leftrightarrow x \in B) \land (x \in A \to (y = D \leftrightarrow y = E))) \to ((x \in A \land y = D) \leftrightarrow (x \in B \land y = E))) \to (\neg (x \in A \lor \neg x \in B) \to ((x \in A \leftrightarrow x \in B) \land (x \in A \to (y = D \leftrightarrow y = E))))$
31		tsbi3	$⊢ \neg (((x \in A \leftrightarrow x \in B) \land (x \in A \to (y = D \leftrightarrow y = E))) \to ((x \in A \land y = D) \leftrightarrow (x \in B \land y = E))) \to ((x \in A \lor \neg x \in B) \lor \neg (x \in A \leftrightarrow x \in B))$
32	31	ord	$⊢ \neg (((x \in A \leftrightarrow x \in B) \land (x \in A \to (y = D \leftrightarrow y = E))) \to ((x \in A \land y = D) \leftrightarrow (x \in B \land y = E))) \to (\neg (x \in A \lor \neg x \in B) \to \neg (x \in A \leftrightarrow x \in B))$
33		tsan2	$⊢ \neg (((x \in A \leftrightarrow x \in B) \land (x \in A \to (y = D \leftrightarrow y = E))) \to ((x \in A \land y = D) \leftrightarrow (x \in B \land y = E))) \to ((x \in A \leftrightarrow x \in B) \lor \neg ((x \in A \leftrightarrow x \in B) \land (x \in A \to (y = D \leftrightarrow y = E))))$
34	33	a1d	$⊢ \neg (((x \in A \leftrightarrow x \in B) \land (x \in A \to (y = D \leftrightarrow y = E))) \to ((x \in A \land y = D) \leftrightarrow (x \in B \land y = E))) \to (\neg (x \in A \lor \neg x \in B) \to ((x \in A \leftrightarrow x \in B) \lor \neg ((x \in A \leftrightarrow x \in B) \land (x \in A \to (y = D \leftrightarrow y = E)))))$
35	32 34	cnf1dd	$⊢ \neg (((x \in A \leftrightarrow x \in B) \land (x \in A \to (y = D \leftrightarrow y = E))) \to ((x \in A \land y = D) \leftrightarrow (x \in B \land y = E))) \to (\neg (x \in A \lor \neg x \in B) \to \neg ((x \in A \leftrightarrow x \in B) \land (x \in A \to (y = D \leftrightarrow y = E))))$
36	30 35	contrd	$⊢ \neg (((x \in A \leftrightarrow x \in B) \land (x \in A \to (y = D \leftrightarrow y = E))) \to ((x \in A \land y = D) \leftrightarrow (x \in B \land y = E))) \to (x \in A \lor \neg x \in B)$
37	36	ord	$⊢ \neg (((x \in A \leftrightarrow x \in B) \land (x \in A \to (y = D \leftrightarrow y = E))) \to ((x \in A \land y = D) \leftrightarrow (x \in B \land y = E))) \to (\neg x \in A \to \neg x \in B)$
38		tsan2	$⊢ \neg (((x \in A \leftrightarrow x \in B) \land (x \in A \to (y = D \leftrightarrow y = E))) \to ((x \in A \land y = D) \leftrightarrow (x \in B \land y = E))) \to (x \in B \lor \neg (x \in B \land y = E))$
39	38	a1d	$⊢ \neg (((x \in A \leftrightarrow x \in B) \land (x \in A \to (y = D \leftrightarrow y = E))) \to ((x \in A \land y = D) \leftrightarrow (x \in B \land y = E))) \to (\neg x \in A \to (x \in B \lor \neg (x \in B \land y = E)))$
40	37 39	cnf1dd	$⊢ \neg (((x \in A \leftrightarrow x \in B) \land (x \in A \to (y = D \leftrightarrow y = E))) \to ((x \in A \land y = D) \leftrightarrow (x \in B \land y = E))) \to (\neg x \in A \to \neg (x \in B \land y = E))$
41	28 40	contrd	$⊢ \neg (((x \in A \leftrightarrow x \in B) \land (x \in A \to (y = D \leftrightarrow y = E))) \to ((x \in A \land y = D) \leftrightarrow (x \in B \land y = E))) \to x \in A$
42	41	a1d	$⊢ \neg (((x \in A \leftrightarrow x \in B) \land (x \in A \to (y = D \leftrightarrow y = E))) \to ((x \in A \land y = D) \leftrightarrow (x \in B \land y = E))) \to (\neg ⊥ \to x \in A)$
43	29	a1d	$⊢ \neg (((x \in A \leftrightarrow x \in B) \land (x \in A \to (y = D \leftrightarrow y = E))) \to ((x \in A \land y = D) \leftrightarrow (x \in B \land y = E))) \to (\neg ⊥ \to ((x \in A \leftrightarrow x \in B) \land (x \in A \to (y = D \leftrightarrow y = E))))$
44		tsan3	$⊢ \neg (((x \in A \leftrightarrow x \in B) \land (x \in A \to (y = D \leftrightarrow y = E))) \to ((x \in A \land y = D) \leftrightarrow (x \in B \land y = E))) \to ((x \in A \to (y = D \leftrightarrow y = E)) \lor \neg ((x \in A \leftrightarrow x \in B) \land (x \in A \to (y = D \leftrightarrow y = E))))$
45	44	a1d	$⊢ \neg (((x \in A \leftrightarrow x \in B) \land (x \in A \to (y = D \leftrightarrow y = E))) \to ((x \in A \land y = D) \leftrightarrow (x \in B \land y = E))) \to (\neg ⊥ \to ((x \in A \to (y = D \leftrightarrow y = E)) \lor \neg ((x \in A \leftrightarrow x \in B) \land (x \in A \to (y = D \leftrightarrow y = E)))))$
46	43 45	cnfn2dd	$⊢ \neg (((x \in A \leftrightarrow x \in B) \land (x \in A \to (y = D \leftrightarrow y = E))) \to ((x \in A \land y = D) \leftrightarrow (x \in B \land y = E))) \to (\neg ⊥ \to (x \in A \to (y = D \leftrightarrow y = E)))$
47	42 46	mpdd	$⊢ \neg (((x \in A \leftrightarrow x \in B) \land (x \in A \to (y = D \leftrightarrow y = E))) \to ((x \in A \land y = D) \leftrightarrow (x \in B \land y = E))) \to (\neg ⊥ \to (y = D \leftrightarrow y = E))$
48		notnotr	$⊢ \neg \neg (x \in B \land y = E) \to (x \in B \land y = E)$
49	48	a1i	$⊢ \neg (((x \in A \leftrightarrow x \in B) \land (x \in A \to (y = D \leftrightarrow y = E))) \to ((x \in A \land y = D) \leftrightarrow (x \in B \land y = E))) \to (\neg \neg (x \in B \land y = E) \to (x \in B \land y = E))$
50	38	a1d	$⊢ \neg (((x \in A \leftrightarrow x \in B) \land (x \in A \to (y = D \leftrightarrow y = E))) \to ((x \in A \land y = D) \leftrightarrow (x \in B \land y = E))) \to (\neg \neg (x \in B \land y = E) \to (x \in B \lor \neg (x \in B \land y = E)))$
51	49 50	cnfn2dd	$⊢ \neg (((x \in A \leftrightarrow x \in B) \land (x \in A \to (y = D \leftrightarrow y = E))) \to ((x \in A \land y = D) \leftrightarrow (x \in B \land y = E))) \to (\neg \neg (x \in B \land y = E) \to x \in B)$
52	36	a1d	$⊢ \neg (((x \in A \leftrightarrow x \in B) \land (x \in A \to (y = D \leftrightarrow y = E))) \to ((x \in A \land y = D) \leftrightarrow (x \in B \land y = E))) \to (\neg \neg (x \in B \land y = E) \to (x \in A \lor \neg x \in B))$
53	51 52	cnfn2dd	$⊢ \neg (((x \in A \leftrightarrow x \in B) \land (x \in A \to (y = D \leftrightarrow y = E))) \to ((x \in A \land y = D) \leftrightarrow (x \in B \land y = E))) \to (\neg \neg (x \in B \land y = E) \to x \in A)$
54		tsan3	$⊢ \neg (((x \in A \leftrightarrow x \in B) \land (x \in A \to (y = D \leftrightarrow y = E))) \to ((x \in A \land y = D) \leftrightarrow (x \in B \land y = E))) \to (y = E \lor \neg (x \in B \land y = E))$
55	54	a1d	$⊢ \neg (((x \in A \leftrightarrow x \in B) \land (x \in A \to (y = D \leftrightarrow y = E))) \to ((x \in A \land y = D) \leftrightarrow (x \in B \land y = E))) \to (\neg \neg (x \in B \land y = E) \to (y = E \lor \neg (x \in B \land y = E)))$
56	49 55	cnfn2dd	$⊢ \neg (((x \in A \leftrightarrow x \in B) \land (x \in A \to (y = D \leftrightarrow y = E))) \to ((x \in A \land y = D) \leftrightarrow (x \in B \land y = E))) \to (\neg \neg (x \in B \land y = E) \to y = E)$
57	29	a1d	$⊢ \neg (((x \in A \leftrightarrow x \in B) \land (x \in A \to (y = D \leftrightarrow y = E))) \to ((x \in A \land y = D) \leftrightarrow (x \in B \land y = E))) \to (\neg \neg (x \in B \land y = E) \to ((x \in A \leftrightarrow x \in B) \land (x \in A \to (y = D \leftrightarrow y = E))))$
58	44	a1d	$⊢ \neg (((x \in A \leftrightarrow x \in B) \land (x \in A \to (y = D \leftrightarrow y = E))) \to ((x \in A \land y = D) \leftrightarrow (x \in B \land y = E))) \to (\neg \neg (x \in B \land y = E) \to ((x \in A \to (y = D \leftrightarrow y = E)) \lor \neg ((x \in A \leftrightarrow x \in B) \land (x \in A \to (y = D \leftrightarrow y = E)))))$
59	57 58	cnfn2dd	$⊢ \neg (((x \in A \leftrightarrow x \in B) \land (x \in A \to (y = D \leftrightarrow y = E))) \to ((x \in A \land y = D) \leftrightarrow (x \in B \land y = E))) \to (\neg \neg (x \in B \land y = E) \to (x \in A \to (y = D \leftrightarrow y = E)))$
60	53 59	mpdd	$⊢ \neg (((x \in A \leftrightarrow x \in B) \land (x \in A \to (y = D \leftrightarrow y = E))) \to ((x \in A \land y = D) \leftrightarrow (x \in B \land y = E))) \to (\neg \neg (x \in B \land y = E) \to (y = D \leftrightarrow y = E))$
61		tsbi3	$⊢ \neg (((x \in A \leftrightarrow x \in B) \land (x \in A \to (y = D \leftrightarrow y = E))) \to ((x \in A \land y = D) \leftrightarrow (x \in B \land y = E))) \to ((y = D \lor \neg y = E) \lor \neg (y = D \leftrightarrow y = E))$
62	61	a1d	$⊢ \neg (((x \in A \leftrightarrow x \in B) \land (x \in A \to (y = D \leftrightarrow y = E))) \to ((x \in A \land y = D) \leftrightarrow (x \in B \land y = E))) \to (\neg \neg (x \in B \land y = E) \to ((y = D \lor \neg y = E) \lor \neg (y = D \leftrightarrow y = E)))$
63	60 62	cnfn2dd	$⊢ \neg (((x \in A \leftrightarrow x \in B) \land (x \in A \to (y = D \leftrightarrow y = E))) \to ((x \in A \land y = D) \leftrightarrow (x \in B \land y = E))) \to (\neg \neg (x \in B \land y = E) \to (y = D \lor \neg y = E))$
64	56 63	cnfn2dd	$⊢ \neg (((x \in A \leftrightarrow x \in B) \land (x \in A \to (y = D \leftrightarrow y = E))) \to ((x \in A \land y = D) \leftrightarrow (x \in B \land y = E))) \to (\neg \neg (x \in B \land y = E) \to y = D)$
65	53 64	jcad	$⊢ \neg (((x \in A \leftrightarrow x \in B) \land (x \in A \to (y = D \leftrightarrow y = E))) \to ((x \in A \land y = D) \leftrightarrow (x \in B \land y = E))) \to (\neg \neg (x \in B \land y = E) \to (x \in A \land y = D))$
66		ax-1	$⊢ \neg (((x \in A \leftrightarrow x \in B) \land (x \in A \to (y = D \leftrightarrow y = E))) \to ((x \in A \land y = D) \leftrightarrow (x \in B \land y = E))) \to (\neg \neg (x \in B \land y = E) \to \neg (((x \in A \leftrightarrow x \in B) \land (x \in A \to (y = D \leftrightarrow y = E))) \to ((x \in A \land y = D) \leftrightarrow (x \in B \land y = E))))$
67		tsim3	$⊢ \neg (((x \in A \leftrightarrow x \in B) \land (x \in A \to (y = D \leftrightarrow y = E))) \to ((x \in A \land y = D) \leftrightarrow (x \in B \land y = E))) \to (\neg ((x \in A \land y = D) \leftrightarrow (x \in B \land y = E)) \lor (((x \in A \leftrightarrow x \in B) \land (x \in A \to (y = D \leftrightarrow y = E))) \to ((x \in A \land y = D) \leftrightarrow (x \in B \land y = E))))$
68	67	a1d	$⊢ \neg (((x \in A \leftrightarrow x \in B) \land (x \in A \to (y = D \leftrightarrow y = E))) \to ((x \in A \land y = D) \leftrightarrow (x \in B \land y = E))) \to (\neg \neg (x \in B \land y = E) \to (\neg ((x \in A \land y = D) \leftrightarrow (x \in B \land y = E)) \lor (((x \in A \leftrightarrow x \in B) \land (x \in A \to (y = D \leftrightarrow y = E))) \to ((x \in A \land y = D) \leftrightarrow (x \in B \land y = E)))))$
69	66 68	cnf2dd	$⊢ \neg (((x \in A \leftrightarrow x \in B) \land (x \in A \to (y = D \leftrightarrow y = E))) \to ((x \in A \land y = D) \leftrightarrow (x \in B \land y = E))) \to (\neg \neg (x \in B \land y = E) \to \neg ((x \in A \land y = D) \leftrightarrow (x \in B \land y = E)))$
70		tsbi1	$⊢ \neg (((x \in A \leftrightarrow x \in B) \land (x \in A \to (y = D \leftrightarrow y = E))) \to ((x \in A \land y = D) \leftrightarrow (x \in B \land y = E))) \to ((\neg (x \in A \land y = D) \lor \neg (x \in B \land y = E)) \lor ((x \in A \land y = D) \leftrightarrow (x \in B \land y = E)))$
71	70	a1d	$⊢ \neg (((x \in A \leftrightarrow x \in B) \land (x \in A \to (y = D \leftrightarrow y = E))) \to ((x \in A \land y = D) \leftrightarrow (x \in B \land y = E))) \to (\neg \neg (x \in B \land y = E) \to ((\neg (x \in A \land y = D) \lor \neg (x \in B \land y = E)) \lor ((x \in A \land y = D) \leftrightarrow (x \in B \land y = E))))$
72	69 71	cnf2dd	$⊢ \neg (((x \in A \leftrightarrow x \in B) \land (x \in A \to (y = D \leftrightarrow y = E))) \to ((x \in A \land y = D) \leftrightarrow (x \in B \land y = E))) \to (\neg \neg (x \in B \land y = E) \to (\neg (x \in A \land y = D) \lor \neg (x \in B \land y = E)))$
73	49 72	cnfn2dd	$⊢ \neg (((x \in A \leftrightarrow x \in B) \land (x \in A \to (y = D \leftrightarrow y = E))) \to ((x \in A \land y = D) \leftrightarrow (x \in B \land y = E))) \to (\neg \neg (x \in B \land y = E) \to \neg (x \in A \land y = D))$
74	65 73	contrd	$⊢ \neg (((x \in A \leftrightarrow x \in B) \land (x \in A \to (y = D \leftrightarrow y = E))) \to ((x \in A \land y = D) \leftrightarrow (x \in B \land y = E))) \to \neg (x \in B \land y = E)$
75	74	a1d	$⊢ \neg (((x \in A \leftrightarrow x \in B) \land (x \in A \to (y = D \leftrightarrow y = E))) \to ((x \in A \land y = D) \leftrightarrow (x \in B \land y = E))) \to (\neg ⊥ \to \neg (x \in B \land y = E))$
76	26	a1d	$⊢ \neg (((x \in A \leftrightarrow x \in B) \land (x \in A \to (y = D \leftrightarrow y = E))) \to ((x \in A \land y = D) \leftrightarrow (x \in B \land y = E))) \to (\neg ⊥ \to ((x \in A \land y = D) \lor (x \in B \land y = E)))$
77	75 76	cnf2dd	$⊢ \neg (((x \in A \leftrightarrow x \in B) \land (x \in A \to (y = D \leftrightarrow y = E))) \to ((x \in A \land y = D) \leftrightarrow (x \in B \land y = E))) \to (\neg ⊥ \to (x \in A \land y = D))$
78		tsan3	$⊢ \neg (((x \in A \leftrightarrow x \in B) \land (x \in A \to (y = D \leftrightarrow y = E))) \to ((x \in A \land y = D) \leftrightarrow (x \in B \land y = E))) \to (y = D \lor \neg (x \in A \land y = D))$
79	78	a1d	$⊢ \neg (((x \in A \leftrightarrow x \in B) \land (x \in A \to (y = D \leftrightarrow y = E))) \to ((x \in A \land y = D) \leftrightarrow (x \in B \land y = E))) \to (\neg ⊥ \to (y = D \lor \neg (x \in A \land y = D)))$
80	77 79	cnfn2dd	$⊢ \neg (((x \in A \leftrightarrow x \in B) \land (x \in A \to (y = D \leftrightarrow y = E))) \to ((x \in A \land y = D) \leftrightarrow (x \in B \land y = E))) \to (\neg ⊥ \to y = D)$
81	33	a1d	$⊢ \neg (((x \in A \leftrightarrow x \in B) \land (x \in A \to (y = D \leftrightarrow y = E))) \to ((x \in A \land y = D) \leftrightarrow (x \in B \land y = E))) \to (\neg ⊥ \to ((x \in A \leftrightarrow x \in B) \lor \neg ((x \in A \leftrightarrow x \in B) \land (x \in A \to (y = D \leftrightarrow y = E)))))$
82	43 81	cnfn2dd	$⊢ \neg (((x \in A \leftrightarrow x \in B) \land (x \in A \to (y = D \leftrightarrow y = E))) \to ((x \in A \land y = D) \leftrightarrow (x \in B \land y = E))) \to (\neg ⊥ \to (x \in A \leftrightarrow x \in B))$
83		tsbi4	$⊢ \neg (((x \in A \leftrightarrow x \in B) \land (x \in A \to (y = D \leftrightarrow y = E))) \to ((x \in A \land y = D) \leftrightarrow (x \in B \land y = E))) \to ((\neg x \in A \lor x \in B) \lor \neg (x \in A \leftrightarrow x \in B))$
84	83	a1d	$⊢ \neg (((x \in A \leftrightarrow x \in B) \land (x \in A \to (y = D \leftrightarrow y = E))) \to ((x \in A \land y = D) \leftrightarrow (x \in B \land y = E))) \to (\neg ⊥ \to ((\neg x \in A \lor 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 (x \in A \to (y = D \leftrightarrow y = E))) \to ((x \in A \land y = D) \leftrightarrow (x \in B \land y = E))) \to (\neg ⊥ \to (\neg x \in A \lor x \in B))$
86	42 85	cnfn1dd	$⊢ \neg (((x \in A \leftrightarrow x \in B) \land (x \in A \to (y = D \leftrightarrow y = E))) \to ((x \in A \land y = D) \leftrightarrow (x \in B \land y = E))) \to (\neg ⊥ \to x \in B)$
87		tsan1	$⊢ \neg (((x \in A \leftrightarrow x \in B) \land (x \in A \to (y = D \leftrightarrow y = E))) \to ((x \in A \land y = D) \leftrightarrow (x \in B \land y = E))) \to ((\neg x \in B \lor \neg y = E) \lor (x \in B \land y = E))$
88	87	a1d	$⊢ \neg (((x \in A \leftrightarrow x \in B) \land (x \in A \to (y = D \leftrightarrow y = E))) \to ((x \in A \land y = D) \leftrightarrow (x \in B \land y = E))) \to (\neg ⊥ \to ((\neg x \in B \lor \neg y = E) \lor (x \in B \land y = E)))$
89	75 88	cnf2dd	$⊢ \neg (((x \in A \leftrightarrow x \in B) \land (x \in A \to (y = D \leftrightarrow y = E))) \to ((x \in A \land y = D) \leftrightarrow (x \in B \land y = E))) \to (\neg ⊥ \to (\neg x \in B \lor \neg y = E))$
90	86 89	cnfn1dd	$⊢ \neg (((x \in A \leftrightarrow x \in B) \land (x \in A \to (y = D \leftrightarrow y = E))) \to ((x \in A \land y = D) \leftrightarrow (x \in B \land y = E))) \to (\neg ⊥ \to \neg y = E)$
91		tsbi4	$⊢ \neg (((x \in A \leftrightarrow x \in B) \land (x \in A \to (y = D \leftrightarrow y = E))) \to ((x \in A \land y = D) \leftrightarrow (x \in B \land y = E))) \to ((\neg y = D \lor y = E) \lor \neg (y = D \leftrightarrow y = E))$
92	91	a1d	$⊢ \neg (((x \in A \leftrightarrow x \in B) \land (x \in A \to (y = D \leftrightarrow y = E))) \to ((x \in A \land y = D) \leftrightarrow (x \in B \land y = E))) \to (\neg ⊥ \to ((\neg y = D \lor y = E) \lor \neg (y = D \leftrightarrow y = E)))$
93	92	or32dd	$⊢ \neg (((x \in A \leftrightarrow x \in B) \land (x \in A \to (y = D \leftrightarrow y = E))) \to ((x \in A \land y = D) \leftrightarrow (x \in B \land y = E))) \to (\neg ⊥ \to ((\neg y = D \lor \neg (y = D \leftrightarrow y = E)) \lor y = E))$
94	90 93	cnf2dd	$⊢ \neg (((x \in A \leftrightarrow x \in B) \land (x \in A \to (y = D \leftrightarrow y = E))) \to ((x \in A \land y = D) \leftrightarrow (x \in B \land y = E))) \to (\neg ⊥ \to (\neg y = D \lor \neg (y = D \leftrightarrow y = E)))$
95	80 94	cnfn1dd	$⊢ \neg (((x \in A \leftrightarrow x \in B) \land (x \in A \to (y = D \leftrightarrow y = E))) \to ((x \in A \land y = D) \leftrightarrow (x \in B \land y = E))) \to (\neg ⊥ \to \neg (y = D \leftrightarrow y = E))$
96	47 95	contrd	$⊢ \neg (((x \in A \leftrightarrow x \in B) \land (x \in A \to (y = D \leftrightarrow y = E))) \to ((x \in A \land y = D) \leftrightarrow (x \in B \land y = E))) \to ⊥$
97	96	efald2	$⊢ ((x \in A \leftrightarrow x \in B) \land (x \in A \to (y = D \leftrightarrow y = E))) \to ((x \in A \land y = D) \leftrightarrow (x \in B \land y = E))$
98	97	2alimi	$⊢ \forall x \forall y ((x \in A \leftrightarrow x \in B) \land (x \in A \to (y = D \leftrightarrow y = E))) \to \forall x \forall y ((x \in A \land y = D) \leftrightarrow (x \in B \land y = E))$
99	19 98	syl	$⊢ (A = B \land \forall x \in A D = E) \to \forall x \forall y ((x \in A \land y = D) \leftrightarrow (x \in B \land y = E))$
100		eqopab2bw	$⊢ \{⟨x, y⟩ \| (x \in A \land y = D)\} = \{⟨x, y⟩ \| (x \in B \land y = E)\} \leftrightarrow \forall x \forall y ((x \in A \land y = D) \leftrightarrow (x \in B \land y = E))$
101	99 100	sylibr	$⊢ (A = B \land \forall x \in A D = E) \to \{⟨x, y⟩ \| (x \in A \land y = D)\} = \{⟨x, y⟩ \| (x \in B \land y = E)\}$
102		df-mpt	$⊢ (x \in A ⟼ D) = \{⟨x, y⟩ \| (x \in A \land y = D)\}$
103		df-mpt	$⊢ (x \in B ⟼ E) = \{⟨x, y⟩ \| (x \in B \land y = E)\}$
104	101 102 103	3eqtr4g	$⊢ (A = B \land \forall x \in A D = E) \to (x \in A ⟼ D) = (x \in B ⟼ E)$

Metamath Proof Explorer

Theorem mptbi12f

Proof