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 ) |
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 ) |