Theorem bj-fvmptunsn2

Description: Value of a function expressed as a union of a mapsto expression and a singleton on a couple (with disjoint domain) at a point in the domain of the mapsto construction. (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-fvmptunsn2.el	|- ( ph -> E e. A )
	bj-fvmptunsn2.ex	|- ( ph -> G e. V )
	bj-fvmptunsn2.is	|- ( ( ph /\ x = E ) -> B = G )
Assertion	bj-fvmptunsn2	|- ( ph -> ( F ` E ) = G )

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-fvmptunsn2.el	|- ( ph -> E e. A )
4		bj-fvmptunsn2.ex	|- ( ph -> G e. V )
5		bj-fvmptunsn2.is	|- ( ( ph /\ x = E ) -> B = G )
6		nelneq	|- ( ( E e. A /\ -. C e. A ) -> -. E = C )
7	3 2 6	syl2anc	|- ( ph -> -. E = C )
8	1 7	bj-fununsn1	|- ( ph -> ( F ` E ) = ( ( x e. A |-> B ) ` E ) )
9		eqidd	|- ( ph -> ( x e. A |-> B ) = ( x e. A |-> B ) )
10	9 5 3 4	fvmptd	|- ( ph -> ( ( x e. A |-> B ) ` E ) = G )
11	8 10	eqtrd	|- ( ph -> ( F ` E ) = G )