This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑦 ∈ 𝐴 ↦ 𝐶 )