Theorem bj-fvmptunsn1

Description: Value of a function expressed as a union of a mapsto expression and a singleton on a couple (with disjoint domain) at the first component of that couple. (Contributed by BJ, 18-Mar-2023) (Proof modification is discouraged.)

	Ref	Expression
Hypotheses	bj-fvmptunsn.un	|- ( ph -> F = ( ( x e. A |-> B ) u. { <. C , D >. } ) )
	bj-fvmptunsn.nel	|- ( ph -> -. C e. A )
	bj-fvmptunsn1.ex1	|- ( ph -> C e. V )
	bj-fvmptunsn1.ex2	|- ( ph -> D e. W )
Assertion	bj-fvmptunsn1	|- ( ph -> ( F ` C ) = D )

Proof

Step	Hyp	Ref	Expression
1		bj-fvmptunsn.un	|- ( ph -> F = ( ( x e. A |-> B ) u. { <. C , D >. } ) )
2		bj-fvmptunsn.nel	|- ( ph -> -. C e. A )
3		bj-fvmptunsn1.ex1	|- ( ph -> C e. V )
4		bj-fvmptunsn1.ex2	|- ( ph -> D e. W )
5		eqid	|- ( x e. A |-> B ) = ( x e. A |-> B )
6	5	dmmptss	|- dom ( x e. A |-> B ) C_ A
7	6	sseli	|- ( C e. dom ( x e. A |-> B ) -> C e. A )
8	2 7	nsyl	|- ( ph -> -. C e. dom ( x e. A |-> B ) )
9	1 8 3 4	bj-fununsn2	|- ( ph -> ( F ` C ) = D )