cbvmpox2

Description: Rule to change the bound variable in a maps-to function, using implicit substitution. This version of cbvmpo allows A to be a function of y , analogous to cbvmpox . (Contributed by AV, 30-Mar-2019)

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

Proof

Step	Hyp	Ref	Expression
1		cbvmpox2.1	$⊢ \underline{Ⅎ} z A$
2		cbvmpox2.2	$⊢ \underline{Ⅎ} y D$
3		cbvmpox2.3	$⊢ \underline{Ⅎ} z C$
4		cbvmpox2.4	$⊢ \underline{Ⅎ} w C$
5		cbvmpox2.5	$⊢ \underline{Ⅎ} x E$
6		cbvmpox2.6	$⊢ \underline{Ⅎ} y E$
7		cbvmpox2.7	$⊢ y = z \to A = D$
8		cbvmpox2.8	$⊢ (y = z \land x = w) \to C = E$
9		nfv	$⊢ Ⅎ w x \in A$
10		nfv	$⊢ Ⅎ w y \in B$
11	9 10	nfan	$⊢ Ⅎ w (x \in A \land y \in B)$
12	4	nfeq2	$⊢ Ⅎ w u = C$
13	11 12	nfan	$⊢ Ⅎ w ((x \in A \land y \in B) \land u = C)$
14	1	nfcri	$⊢ Ⅎ z x \in A$
15		nfv	$⊢ Ⅎ z y \in B$
16	14 15	nfan	$⊢ Ⅎ z (x \in A \land y \in B)$
17	3	nfeq2	$⊢ Ⅎ z u = C$
18	16 17	nfan	$⊢ Ⅎ z ((x \in A \land y \in B) \land u = C)$
19		nfv	$⊢ Ⅎ x w \in D$
20		nfv	$⊢ Ⅎ x z \in B$
21	19 20	nfan	$⊢ Ⅎ x (w \in D \land z \in B)$
22	5	nfeq2	$⊢ Ⅎ x u = E$
23	21 22	nfan	$⊢ Ⅎ x ((w \in D \land z \in B) \land u = E)$
24	2	nfcri	$⊢ Ⅎ y w \in D$
25		nfv	$⊢ Ⅎ y z \in B$
26	24 25	nfan	$⊢ Ⅎ y (w \in D \land z \in B)$
27	6	nfeq2	$⊢ Ⅎ y u = E$
28	26 27	nfan	$⊢ Ⅎ y ((w \in D \land z \in B) \land u = E)$
29		eleq1w	$⊢ x = w \to (x \in A \leftrightarrow w \in A)$
30	7	eleq2d	$⊢ y = z \to (w \in A \leftrightarrow w \in D)$
31	29 30	sylan9bb	$⊢ (x = w \land y = z) \to (x \in A \leftrightarrow w \in D)$
32		simpr	$⊢ (x = w \land y = z) \to y = z$
33	32	eleq1d	$⊢ (x = w \land y = z) \to (y \in B \leftrightarrow z \in B)$
34	31 33	anbi12d	$⊢ (x = w \land y = z) \to ((x \in A \land y \in B) \leftrightarrow (w \in D \land z \in B))$
35	8	ancoms	$⊢ (x = w \land y = z) \to C = E$
36	35	eqeq2d	$⊢ (x = w \land y = z) \to (u = C \leftrightarrow u = E)$
37	34 36	anbi12d	$⊢ (x = w \land y = z) \to (((x \in A \land y \in B) \land u = C) \leftrightarrow ((w \in D \land z \in B) \land u = E))$
38	13 18 23 28 37	cbvoprab12	$⊢ \{⟨⟨x, y⟩, u⟩ \| ((x \in A \land y \in B) \land u = C)\} = \{⟨⟨w, z⟩, u⟩ \| ((w \in D \land z \in B) \land u = E)\}$
39		df-mpo	$⊢ (x \in A, y \in B ⟼ C) = \{⟨⟨x, y⟩, u⟩ \| ((x \in A \land y \in B) \land u = C)\}$
40		df-mpo	$⊢ (w \in D, z \in B ⟼ E) = \{⟨⟨w, z⟩, u⟩ \| ((w \in D \land z \in B) \land u = E)\}$
41	38 39 40	3eqtr4i	$⊢ (x \in A, y \in B ⟼ C) = (w \in D, z \in B ⟼ E)$

Metamath Proof Explorer

Theorem cbvmpox2

Proof