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 e. { X } , j e. B |-> if ( i = X , C , D ) ) = ( i e. { X } , j e. B |-> C )

Proof

Step Hyp Ref Expression
1 elsni
 |-  ( i e. { X } -> i = X )
2 1 adantr
 |-  ( ( i e. { X } /\ j e. B ) -> i = X )
3 2 iftrued
 |-  ( ( i e. { X } /\ j e. B ) -> if ( i = X , C , D ) = C )
4 3 mpoeq3ia
 |-  ( i e. { X } , j e. B |-> if ( i = X , C , D ) ) = ( i e. { X } , j e. B |-> C )