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	⊢ Ⅎ 𝑧 𝐵
	cbvmpox.2	⊢ Ⅎ 𝑥 𝐷
	cbvmpox.3	⊢ Ⅎ 𝑧 𝐶
	cbvmpox.4	⊢ Ⅎ 𝑤 𝐶
	cbvmpox.5	⊢ Ⅎ 𝑥 𝐸
	cbvmpox.6	⊢ Ⅎ 𝑦 𝐸
	cbvmpox.7	⊢ ( 𝑥 = 𝑧 → 𝐵 = 𝐷 )
	cbvmpox.8	⊢ ( ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) → 𝐶 = 𝐸 )
Assertion	cbvmpox	⊢ ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) = ( 𝑧 ∈ 𝐴 , 𝑤 ∈ 𝐷 ↦ 𝐸 )

Proof

Step	Hyp	Ref	Expression
1		cbvmpox.1	⊢ Ⅎ 𝑧 𝐵
2		cbvmpox.2	⊢ Ⅎ 𝑥 𝐷
3		cbvmpox.3	⊢ Ⅎ 𝑧 𝐶
4		cbvmpox.4	⊢ Ⅎ 𝑤 𝐶
5		cbvmpox.5	⊢ Ⅎ 𝑥 𝐸
6		cbvmpox.6	⊢ Ⅎ 𝑦 𝐸
7		cbvmpox.7	⊢ ( 𝑥 = 𝑧 → 𝐵 = 𝐷 )
8		cbvmpox.8	⊢ ( ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) → 𝐶 = 𝐸 )
9		nfv	⊢ Ⅎ 𝑧 𝑥 ∈ 𝐴
10	1	nfcri	⊢ Ⅎ 𝑧 𝑦 ∈ 𝐵
11	9 10	nfan	⊢ Ⅎ 𝑧 ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 )
12	3	nfeq2	⊢ Ⅎ 𝑧 𝑢 = 𝐶
13	11 12	nfan	⊢ Ⅎ 𝑧 ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑢 = 𝐶 )
14		nfv	⊢ Ⅎ 𝑤 𝑥 ∈ 𝐴
15		nfcv	⊢ Ⅎ 𝑤 𝐵
16	15	nfcri	⊢ Ⅎ 𝑤 𝑦 ∈ 𝐵
17	14 16	nfan	⊢ Ⅎ 𝑤 ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 )
18	4	nfeq2	⊢ Ⅎ 𝑤 𝑢 = 𝐶
19	17 18	nfan	⊢ Ⅎ 𝑤 ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑢 = 𝐶 )
20		nfv	⊢ Ⅎ 𝑥 𝑧 ∈ 𝐴
21	2	nfcri	⊢ Ⅎ 𝑥 𝑤 ∈ 𝐷
22	20 21	nfan	⊢ Ⅎ 𝑥 ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐷 )
23	5	nfeq2	⊢ Ⅎ 𝑥 𝑢 = 𝐸
24	22 23	nfan	⊢ Ⅎ 𝑥 ( ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐷 ) ∧ 𝑢 = 𝐸 )
25		nfv	⊢ Ⅎ 𝑦 ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐷 )
26	6	nfeq2	⊢ Ⅎ 𝑦 𝑢 = 𝐸
27	25 26	nfan	⊢ Ⅎ 𝑦 ( ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐷 ) ∧ 𝑢 = 𝐸 )
28		eleq1w	⊢ ( 𝑥 = 𝑧 → ( 𝑥 ∈ 𝐴 ↔ 𝑧 ∈ 𝐴 ) )
29	28	adantr	⊢ ( ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) → ( 𝑥 ∈ 𝐴 ↔ 𝑧 ∈ 𝐴 ) )
30	7	eleq2d	⊢ ( 𝑥 = 𝑧 → ( 𝑦 ∈ 𝐵 ↔ 𝑦 ∈ 𝐷 ) )
31		eleq1w	⊢ ( 𝑦 = 𝑤 → ( 𝑦 ∈ 𝐷 ↔ 𝑤 ∈ 𝐷 ) )
32	30 31	sylan9bb	⊢ ( ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) → ( 𝑦 ∈ 𝐵 ↔ 𝑤 ∈ 𝐷 ) )
33	29 32	anbi12d	⊢ ( ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) → ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ↔ ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐷 ) ) )
34	8	eqeq2d	⊢ ( ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) → ( 𝑢 = 𝐶 ↔ 𝑢 = 𝐸 ) )
35	33 34	anbi12d	⊢ ( ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑢 = 𝐶 ) ↔ ( ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐷 ) ∧ 𝑢 = 𝐸 ) ) )
36	13 19 24 27 35	cbvoprab12	⊢ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑢 ⟩ ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑢 = 𝐶 ) } = { ⟨ ⟨ 𝑧 , 𝑤 ⟩ , 𝑢 ⟩ ∣ ( ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐷 ) ∧ 𝑢 = 𝐸 ) }
37		df-mpo	⊢ ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑢 ⟩ ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑢 = 𝐶 ) }
38		df-mpo	⊢ ( 𝑧 ∈ 𝐴 , 𝑤 ∈ 𝐷 ↦ 𝐸 ) = { ⟨ ⟨ 𝑧 , 𝑤 ⟩ , 𝑢 ⟩ ∣ ( ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐷 ) ∧ 𝑢 = 𝐸 ) }
39	36 37 38	3eqtr4i	⊢ ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) = ( 𝑧 ∈ 𝐴 , 𝑤 ∈ 𝐷 ↦ 𝐸 )

Metamath Proof Explorer

Theorem cbvmpox

Proof