Theorem cbvmptfg

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. Usage of this theorem is discouraged because it depends on ax-13 . See cbvmptf for a version with more disjoint variable conditions, but not requiring ax-13 . (Contributed by NM, 11-Sep-2011) (Revised by Thierry Arnoux, 9-Mar-2017) (New usage is discouraged.)

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

Proof

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