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		sbequ	⊢ ( 𝑤 = 𝑦 → ( [ 𝑤 / 𝑥 ] 𝑧 = 𝐵 ↔ [ 𝑦 / 𝑥 ] 𝑧 = 𝐵 ) )
21	4	nfeq2	⊢ Ⅎ 𝑥 𝑧 = 𝐶
22	5	eqeq2d	⊢ ( 𝑥 = 𝑦 → ( 𝑧 = 𝐵 ↔ 𝑧 = 𝐶 ) )
23	21 22	sbiev	⊢ ( [ 𝑦 / 𝑥 ] 𝑧 = 𝐵 ↔ 𝑧 = 𝐶 )
24	20 23	bitrdi	⊢ ( 𝑤 = 𝑦 → ( [ 𝑤 / 𝑥 ] 𝑧 = 𝐵 ↔ 𝑧 = 𝐶 ) )
25	19 24	anbi12d	⊢ ( 𝑤 = 𝑦 → ( ( 𝑤 ∈ 𝐴 ∧ [ 𝑤 / 𝑥 ] 𝑧 = 𝐵 ) ↔ ( 𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐶 ) ) )
26	17 18 25	cbvopab1	⊢ { ⟨ 𝑤 , 𝑧 ⟩ ∣ ( 𝑤 ∈ 𝐴 ∧ [ 𝑤 / 𝑥 ] 𝑧 = 𝐵 ) } = { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( 𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐶 ) }
27	13 26	eqtri	⊢ { ⟨ 𝑥 , 𝑧 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵 ) } = { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( 𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐶 ) }
28		df-mpt	⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = { ⟨ 𝑥 , 𝑧 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵 ) }
29		df-mpt	⊢ ( 𝑦 ∈ 𝐴 ↦ 𝐶 ) = { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( 𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐶 ) }
30	27 28 29	3eqtr4i	⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑦 ∈ 𝐴 ↦ 𝐶 )