Theorem cbvmptf

Description: Rule to change the bound variable in a maps-to function, using implicit substitution. This version has bound-variable hypotheses in place of distinct variable conditions. (Contributed by NM, 11-Sep-2011) (Revised by Thierry Arnoux, 9-Mar-2017) Add disjoint variable condition to avoid ax-13 . See cbvmptfg for a less restrictive version requiring more axioms. (Revised by GG, 17-Jan-2024)

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

Proof

Step	Hyp	Ref	Expression
1		cbvmptf.1	⊢ Ⅎ 𝑥 𝐴
2		cbvmptf.2	⊢ Ⅎ 𝑦 𝐴
3		cbvmptf.3	⊢ Ⅎ 𝑦 𝐵
4		cbvmptf.4	⊢ Ⅎ 𝑥 𝐶
5		cbvmptf.5	⊢ ( 𝑥 = 𝑦 → 𝐵 = 𝐶 )
6		nfv	⊢ Ⅎ 𝑤 ( 𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵 )
7	1	nfcri	⊢ Ⅎ 𝑥 𝑤 ∈ 𝐴
8		nfs1v	⊢ Ⅎ 𝑥 [ 𝑤 / 𝑥 ] 𝑧 = 𝐵
9	7 8	nfan	⊢ Ⅎ 𝑥 ( 𝑤 ∈ 𝐴 ∧ [ 𝑤 / 𝑥 ] 𝑧 = 𝐵 )
10		eleq1w	⊢ ( 𝑥 = 𝑤 → ( 𝑥 ∈ 𝐴 ↔ 𝑤 ∈ 𝐴 ) )
11		sbequ12	⊢ ( 𝑥 = 𝑤 → ( 𝑧 = 𝐵 ↔ [ 𝑤 / 𝑥 ] 𝑧 = 𝐵 ) )
12	10 11	anbi12d	⊢ ( 𝑥 = 𝑤 → ( ( 𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵 ) ↔ ( 𝑤 ∈ 𝐴 ∧ [ 𝑤 / 𝑥 ] 𝑧 = 𝐵 ) ) )
13	6 9 12	cbvopab1	⊢ { ⟨ 𝑥 , 𝑧 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵 ) } = { ⟨ 𝑤 , 𝑧 ⟩ ∣ ( 𝑤 ∈ 𝐴 ∧ [ 𝑤 / 𝑥 ] 𝑧 = 𝐵 ) }
14	2	nfcri	⊢ Ⅎ 𝑦 𝑤 ∈ 𝐴
15	3	nfeq2	⊢ Ⅎ 𝑦 𝑧 = 𝐵
16	15	nfsbv	⊢ Ⅎ 𝑦 [ 𝑤 / 𝑥 ] 𝑧 = 𝐵
17	14 16	nfan	⊢ Ⅎ 𝑦 ( 𝑤 ∈ 𝐴 ∧ [ 𝑤 / 𝑥 ] 𝑧 = 𝐵 )
18		nfv	⊢ Ⅎ 𝑤 ( 𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐶 )
19		eleq1w	⊢ ( 𝑤 = 𝑦 → ( 𝑤 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴 ) )
20	4	nfeq2	⊢ Ⅎ 𝑥 𝑧 = 𝐶
21	5	eqeq2d	⊢ ( 𝑥 = 𝑦 → ( 𝑧 = 𝐵 ↔ 𝑧 = 𝐶 ) )
22	20 21	sbhypf	⊢ ( 𝑤 = 𝑦 → ( [ 𝑤 / 𝑥 ] 𝑧 = 𝐵 ↔ 𝑧 = 𝐶 ) )
23	19 22	anbi12d	⊢ ( 𝑤 = 𝑦 → ( ( 𝑤 ∈ 𝐴 ∧ [ 𝑤 / 𝑥 ] 𝑧 = 𝐵 ) ↔ ( 𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐶 ) ) )
24	17 18 23	cbvopab1	⊢ { ⟨ 𝑤 , 𝑧 ⟩ ∣ ( 𝑤 ∈ 𝐴 ∧ [ 𝑤 / 𝑥 ] 𝑧 = 𝐵 ) } = { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( 𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐶 ) }
25	13 24	eqtri	⊢ { ⟨ 𝑥 , 𝑧 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵 ) } = { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( 𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐶 ) }
26		df-mpt	⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = { ⟨ 𝑥 , 𝑧 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵 ) }
27		df-mpt	⊢ ( 𝑦 ∈ 𝐴 ↦ 𝐶 ) = { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( 𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐶 ) }
28	25 26 27	3eqtr4i	⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑦 ∈ 𝐴 ↦ 𝐶 )