Metamath Proof Explorer


Theorem cbvmpov

Description: Rule to change the bound variable in a maps-to function, using implicit substitution. With a longer proof analogous to cbvmpt , some distinct variable requirements could be eliminated. (Contributed by NM, 11-Jun-2013)

Ref Expression
Hypotheses cbvmpov.1 ( 𝑥 = 𝑧𝐶 = 𝐸 )
cbvmpov.2 ( 𝑦 = 𝑤𝐸 = 𝐷 )
Assertion cbvmpov ( 𝑥𝐴 , 𝑦𝐵𝐶 ) = ( 𝑧𝐴 , 𝑤𝐵𝐷 )

Proof

Step Hyp Ref Expression
1 cbvmpov.1 ( 𝑥 = 𝑧𝐶 = 𝐸 )
2 cbvmpov.2 ( 𝑦 = 𝑤𝐸 = 𝐷 )
3 eleq1w ( 𝑥 = 𝑧 → ( 𝑥𝐴𝑧𝐴 ) )
4 eleq1w ( 𝑦 = 𝑤 → ( 𝑦𝐵𝑤𝐵 ) )
5 3 4 bi2anan9 ( ( 𝑥 = 𝑧𝑦 = 𝑤 ) → ( ( 𝑥𝐴𝑦𝐵 ) ↔ ( 𝑧𝐴𝑤𝐵 ) ) )
6 1 2 sylan9eq ( ( 𝑥 = 𝑧𝑦 = 𝑤 ) → 𝐶 = 𝐷 )
7 6 eqeq2d ( ( 𝑥 = 𝑧𝑦 = 𝑤 ) → ( 𝑣 = 𝐶𝑣 = 𝐷 ) )
8 5 7 anbi12d ( ( 𝑥 = 𝑧𝑦 = 𝑤 ) → ( ( ( 𝑥𝐴𝑦𝐵 ) ∧ 𝑣 = 𝐶 ) ↔ ( ( 𝑧𝐴𝑤𝐵 ) ∧ 𝑣 = 𝐷 ) ) )
9 8 cbvoprab12v { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑣 ⟩ ∣ ( ( 𝑥𝐴𝑦𝐵 ) ∧ 𝑣 = 𝐶 ) } = { ⟨ ⟨ 𝑧 , 𝑤 ⟩ , 𝑣 ⟩ ∣ ( ( 𝑧𝐴𝑤𝐵 ) ∧ 𝑣 = 𝐷 ) }
10 df-mpo ( 𝑥𝐴 , 𝑦𝐵𝐶 ) = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑣 ⟩ ∣ ( ( 𝑥𝐴𝑦𝐵 ) ∧ 𝑣 = 𝐶 ) }
11 df-mpo ( 𝑧𝐴 , 𝑤𝐵𝐷 ) = { ⟨ ⟨ 𝑧 , 𝑤 ⟩ , 𝑣 ⟩ ∣ ( ( 𝑧𝐴𝑤𝐵 ) ∧ 𝑣 = 𝐷 ) }
12 9 10 11 3eqtr4i ( 𝑥𝐴 , 𝑦𝐵𝐶 ) = ( 𝑧𝐴 , 𝑤𝐵𝐷 )