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 )