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 Gino Giotto, 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 ( 𝑥𝐴𝐵 ) = ( 𝑦𝐴𝐶 )