Theorem 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	⊢ Ⅎ 𝑥 𝐵
	cbvmpo1.2	⊢ Ⅎ 𝑧 𝐵
	cbvmpo1.3	⊢ Ⅎ 𝑧 𝐶
	cbvmpo1.4	⊢ Ⅎ 𝑥 𝐸
	cbvmpo1.5	⊢ ( 𝑥 = 𝑧 → 𝐶 = 𝐸 )
Assertion	cbvmpo1	⊢ ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) = ( 𝑧 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐸 )

Proof

Step	Hyp	Ref	Expression
1		cbvmpo1.1	⊢ Ⅎ 𝑥 𝐵
2		cbvmpo1.2	⊢ Ⅎ 𝑧 𝐵
3		cbvmpo1.3	⊢ Ⅎ 𝑧 𝐶
4		cbvmpo1.4	⊢ Ⅎ 𝑥 𝐸
5		cbvmpo1.5	⊢ ( 𝑥 = 𝑧 → 𝐶 = 𝐸 )
6		nfv	⊢ Ⅎ 𝑧 𝑥 ∈ 𝐴
7	2	nfcri	⊢ Ⅎ 𝑧 𝑦 ∈ 𝐵
8	6 7	nfan	⊢ Ⅎ 𝑧 ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 )
9	3	nfeq2	⊢ Ⅎ 𝑧 𝑢 = 𝐶
10	8 9	nfan	⊢ Ⅎ 𝑧 ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑢 = 𝐶 )
11		nfv	⊢ Ⅎ 𝑥 𝑧 ∈ 𝐴
12	1	nfcri	⊢ Ⅎ 𝑥 𝑦 ∈ 𝐵
13	11 12	nfan	⊢ Ⅎ 𝑥 ( 𝑧 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 )
14	4	nfeq2	⊢ Ⅎ 𝑥 𝑢 = 𝐸
15	13 14	nfan	⊢ Ⅎ 𝑥 ( ( 𝑧 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑢 = 𝐸 )
16		eleq1w	⊢ ( 𝑥 = 𝑧 → ( 𝑥 ∈ 𝐴 ↔ 𝑧 ∈ 𝐴 ) )
17	16	anbi1d	⊢ ( 𝑥 = 𝑧 → ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ↔ ( 𝑧 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) )
18	5	eqeq2d	⊢ ( 𝑥 = 𝑧 → ( 𝑢 = 𝐶 ↔ 𝑢 = 𝐸 ) )
19	17 18	anbi12d	⊢ ( 𝑥 = 𝑧 → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑢 = 𝐶 ) ↔ ( ( 𝑧 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑢 = 𝐸 ) ) )
20	10 15 19	cbvoprab1	⊢ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑢 ⟩ ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑢 = 𝐶 ) } = { ⟨ ⟨ 𝑧 , 𝑦 ⟩ , 𝑢 ⟩ ∣ ( ( 𝑧 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑢 = 𝐸 ) }
21		df-mpo	⊢ ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑢 ⟩ ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑢 = 𝐶 ) }
22		df-mpo	⊢ ( 𝑧 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐸 ) = { ⟨ ⟨ 𝑧 , 𝑦 ⟩ , 𝑢 ⟩ ∣ ( ( 𝑧 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑢 = 𝐸 ) }
23	20 21 22	3eqtr4i	⊢ ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) = ( 𝑧 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐸 )