Theorem mposnif

Description: A mapping with two arguments with the first argument from a singleton and a conditional as result. (Contributed by AV, 14-Feb-2019)

	Ref	Expression
Assertion	mposnif	⊢ ( 𝑖 ∈ { 𝑋 } , 𝑗 ∈ 𝐵 ↦ if ( 𝑖 = 𝑋 , 𝐶 , 𝐷 ) ) = ( 𝑖 ∈ { 𝑋 } , 𝑗 ∈ 𝐵 ↦ 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		elsni	⊢ ( 𝑖 ∈ { 𝑋 } → 𝑖 = 𝑋 )
2	1	adantr	⊢ ( ( 𝑖 ∈ { 𝑋 } ∧ 𝑗 ∈ 𝐵 ) → 𝑖 = 𝑋 )
3	2	iftrued	⊢ ( ( 𝑖 ∈ { 𝑋 } ∧ 𝑗 ∈ 𝐵 ) → if ( 𝑖 = 𝑋 , 𝐶 , 𝐷 ) = 𝐶 )
4	3	mpoeq3ia	⊢ ( 𝑖 ∈ { 𝑋 } , 𝑗 ∈ 𝐵 ↦ if ( 𝑖 = 𝑋 , 𝐶 , 𝐷 ) ) = ( 𝑖 ∈ { 𝑋 } , 𝑗 ∈ 𝐵 ↦ 𝐶 )