Theorem mpodifsnif

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

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

Proof

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