mpoeq123

Description: An equality theorem for the maps-to notation. (Contributed by Mario Carneiro, 16-Dec-2013) (Revised by Mario Carneiro, 19-Mar-2015)

		Ref	Expression
	Assertion	mpoeq123	$⊢ (A = D \land \forall x \in A (B = E \land \forall y \in B C = F)) \to (x \in A, y \in B ⟼ C) = (x \in D, y \in E ⟼ F)$

Proof

Step	Hyp	Ref	Expression
1		nfv	$⊢ Ⅎ x A = D$
2		nfra1	$⊢ Ⅎ x \forall x \in A (B = E \land \forall y \in B C = F)$
3	1 2	nfan	$⊢ Ⅎ x (A = D \land \forall x \in A (B = E \land \forall y \in B C = F))$
4		nfv	$⊢ Ⅎ y A = D$
5		nfcv	$⊢ \underline{Ⅎ} y A$
6		nfv	$⊢ Ⅎ y B = E$
7		nfra1	$⊢ Ⅎ y \forall y \in B C = F$
8	6 7	nfan	$⊢ Ⅎ y (B = E \land \forall y \in B C = F)$
9	5 8	nfralw	$⊢ Ⅎ y \forall x \in A (B = E \land \forall y \in B C = F)$
10	4 9	nfan	$⊢ Ⅎ y (A = D \land \forall x \in A (B = E \land \forall y \in B C = F))$
11		nfv	$⊢ Ⅎ z (A = D \land \forall x \in A (B = E \land \forall y \in B C = F))$
12		rsp	$⊢ \forall x \in A (B = E \land \forall y \in B C = F) \to (x \in A \to (B = E \land \forall y \in B C = F))$
13		rsp	$⊢ \forall y \in B C = F \to (y \in B \to C = F)$
14		eqeq2	$⊢ C = F \to (z = C \leftrightarrow z = F)$
15	13 14	syl6	$⊢ \forall y \in B C = F \to (y \in B \to (z = C \leftrightarrow z = F))$
16	15	pm5.32d	$⊢ \forall y \in B C = F \to ((y \in B \land z = C) \leftrightarrow (y \in B \land z = F))$
17		eleq2	$⊢ B = E \to (y \in B \leftrightarrow y \in E)$
18	17	anbi1d	$⊢ B = E \to ((y \in B \land z = F) \leftrightarrow (y \in E \land z = F))$
19	16 18	sylan9bbr	$⊢ (B = E \land \forall y \in B C = F) \to ((y \in B \land z = C) \leftrightarrow (y \in E \land z = F))$
20	12 19	syl6	$⊢ \forall x \in A (B = E \land \forall y \in B C = F) \to (x \in A \to ((y \in B \land z = C) \leftrightarrow (y \in E \land z = F)))$
21	20	pm5.32d	$⊢ \forall x \in A (B = E \land \forall y \in B C = F) \to ((x \in A \land (y \in B \land z = C)) \leftrightarrow (x \in A \land (y \in E \land z = F)))$
22		eleq2	$⊢ A = D \to (x \in A \leftrightarrow x \in D)$
23	22	anbi1d	$⊢ A = D \to ((x \in A \land (y \in E \land z = F)) \leftrightarrow (x \in D \land (y \in E \land z = F)))$
24	21 23	sylan9bbr	$⊢ (A = D \land \forall x \in A (B = E \land \forall y \in B C = F)) \to ((x \in A \land (y \in B \land z = C)) \leftrightarrow (x \in D \land (y \in E \land z = F)))$
25		anass	$⊢ ((x \in A \land y \in B) \land z = C) \leftrightarrow (x \in A \land (y \in B \land z = C))$
26		anass	$⊢ ((x \in D \land y \in E) \land z = F) \leftrightarrow (x \in D \land (y \in E \land z = F))$
27	24 25 26	3bitr4g	$⊢ (A = D \land \forall x \in A (B = E \land \forall y \in B C = F)) \to (((x \in A \land y \in B) \land z = C) \leftrightarrow ((x \in D \land y \in E) \land z = F))$
28	3 10 11 27	oprabbid	$⊢ (A = D \land \forall x \in A (B = E \land \forall y \in B C = F)) \to \{⟨⟨x, y⟩, z⟩ \| ((x \in A \land y \in B) \land z = C)\} = \{⟨⟨x, y⟩, z⟩ \| ((x \in D \land y \in E) \land z = F)\}$
29		df-mpo	$⊢ (x \in A, y \in B ⟼ C) = \{⟨⟨x, y⟩, z⟩ \| ((x \in A \land y \in B) \land z = C)\}$
30		df-mpo	$⊢ (x \in D, y \in E ⟼ F) = \{⟨⟨x, y⟩, z⟩ \| ((x \in D \land y \in E) \land z = F)\}$
31	28 29 30	3eqtr4g	$⊢ (A = D \land \forall x \in A (B = E \land \forall y \in B C = F)) \to (x \in A, y \in B ⟼ C) = (x \in D, y \in E ⟼ F)$

Metamath Proof Explorer

Theorem mpoeq123

Proof