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

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