# Metamath Proof Explorer

## 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 ¬{i}={X}$
2 1 adantr ${⊢}\left({i}\in \left({A}\setminus \left\{{X}\right\}\right)\wedge {j}\in {B}\right)\to ¬{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)$