Metamath Proof Explorer

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 ⊢ i ∈ X , j ∈ B ⟼ if i = X C D = i ∈ X , j ∈ B ⟼ C

Proof

Step Hyp Ref Expression
1 elsni ⊢ i ∈ X → i = X
2 1 adantr ⊢ i ∈ X ∧ j ∈ B → i = X
3 2 iftrued ⊢ i ∈ X ∧ j ∈ B → if i = X C D = C
4 3 mpoeq3ia ⊢ i ∈ X , j ∈ B ⟼ if i = X C D = i ∈ X , j ∈ B ⟼ C