cbvmpox

Description: Rule to change the bound variable in a maps-to function, using implicit substitution. This version of cbvmpo allows B to be a function of x . (Contributed by NM, 29-Dec-2014)

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

Proof

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

Metamath Proof Explorer

Theorem cbvmpox

Proof