cbvmpo2

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

	Ref	Expression
Hypotheses	cbvmpo2.1	⊢ Ⅎ 𝑦 𝐴
	cbvmpo2.2	⊢ Ⅎ 𝑤 𝐴
	cbvmpo2.3	⊢ Ⅎ 𝑤 𝐶
	cbvmpo2.4	⊢ Ⅎ 𝑦 𝐸
	cbvmpo2.5	⊢ ( 𝑦 = 𝑤 → 𝐶 = 𝐸 )
Assertion	cbvmpo2	⊢ ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) = ( 𝑥 ∈ 𝐴 , 𝑤 ∈ 𝐵 ↦ 𝐸 )

Proof

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

Metamath Proof Explorer

Theorem cbvmpo2

Proof