Metamath Proof Explorer


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