cbvmpo1

Description: Rule to change the first bound variable in a maps-to function, using implicit substitution. (Contributed by Glauco Siliprandi, 26-Jun-2021)

	Ref	Expression
Hypotheses	cbvmpo1.1	$⊢ \underline{Ⅎ} x B$
	cbvmpo1.2	$⊢ \underline{Ⅎ} z B$
	cbvmpo1.3	$⊢ \underline{Ⅎ} z C$
	cbvmpo1.4	$⊢ \underline{Ⅎ} x E$
	cbvmpo1.5	$⊢ x = z \to C = E$
Assertion	cbvmpo1	$⊢ (x \in A, y \in B ⟼ C) = (z \in A, y \in B ⟼ E)$

Proof

Step	Hyp	Ref	Expression
1		cbvmpo1.1	$⊢ \underline{Ⅎ} x B$
2		cbvmpo1.2	$⊢ \underline{Ⅎ} z B$
3		cbvmpo1.3	$⊢ \underline{Ⅎ} z C$
4		cbvmpo1.4	$⊢ \underline{Ⅎ} x E$
5		cbvmpo1.5	$⊢ x = z \to C = E$
6		nfv	$⊢ Ⅎ z x \in A$
7	2	nfcri	$⊢ Ⅎ z y \in B$
8	6 7	nfan	$⊢ Ⅎ z (x \in A \land y \in B)$
9	3	nfeq2	$⊢ Ⅎ z u = C$
10	8 9	nfan	$⊢ Ⅎ z ((x \in A \land y \in B) \land u = C)$
11		nfv	$⊢ Ⅎ x z \in A$
12	1	nfcri	$⊢ Ⅎ x y \in B$
13	11 12	nfan	$⊢ Ⅎ x (z \in A \land y \in B)$
14	4	nfeq2	$⊢ Ⅎ x u = E$
15	13 14	nfan	$⊢ Ⅎ x ((z \in A \land y \in B) \land u = E)$
16		eleq1w	$⊢ x = z \to (x \in A \leftrightarrow z \in A)$
17	16	anbi1d	$⊢ x = z \to ((x \in A \land y \in B) \leftrightarrow (z \in A \land y \in B))$
18	5	eqeq2d	$⊢ x = z \to (u = C \leftrightarrow u = E)$
19	17 18	anbi12d	$⊢ x = z \to (((x \in A \land y \in B) \land u = C) \leftrightarrow ((z \in A \land y \in B) \land u = E))$
20	10 15 19	cbvoprab1	$⊢ \{⟨⟨x, y⟩, u⟩ \| ((x \in A \land y \in B) \land u = C)\} = \{⟨⟨z, y⟩, u⟩ \| ((z \in A \land y \in B) \land u = E)\}$
21		df-mpo	$⊢ (x \in A, y \in B ⟼ C) = \{⟨⟨x, y⟩, u⟩ \| ((x \in A \land y \in B) \land u = C)\}$
22		df-mpo	$⊢ (z \in A, y \in B ⟼ E) = \{⟨⟨z, y⟩, u⟩ \| ((z \in A \land y \in B) \land u = E)\}$
23	20 21 22	3eqtr4i	$⊢ (x \in A, y \in B ⟼ C) = (z \in A, y \in B ⟼ E)$

Metamath Proof Explorer

Theorem cbvmpo1

Proof