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

Proof

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