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	$$⊢\left(i\in \left(A\setminus \left\{X\right\}\right),j\in B⟼if\left(i=X,C,D\right)\right)=\left(i\in \left(A\setminus \left\{X\right\}\right),j\in B⟼D\right)$$

Proof

Step	Hyp	Ref	Expression
1		eldifsnneq	$$⊢i\in \left(A\setminus \left\{X\right\}\right)\to \neg i=X$$
2	1	adantr	$$⊢\left(i\in \left(A\setminus \left\{X\right\}\right)\wedge j\in B\right)\to \neg i=X$$
3	2	iffalsed	$$⊢\left(i\in \left(A\setminus \left\{X\right\}\right)\wedge j\in B\right)\to if\left(i=X,C,D\right)=D$$
4	3	mpoeq3ia	$$⊢\left(i\in \left(A\setminus \left\{X\right\}\right),j\in B⟼if\left(i=X,C,D\right)\right)=\left(i\in \left(A\setminus \left\{X\right\}\right),j\in B⟼D\right)$$