Theorem bj-fununsn2

Description: Value of a function expressed as a union of a function 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-fununsn.un	|- ( ph -> F = ( G u. { <. B , C >. } ) )
	bj-fununsn2.neldm	|- ( ph -> -. B e. dom G )
	bj-fununsn2.ex1	|- ( ph -> B e. V )
	bj-fununsn2.ex2	|- ( ph -> C e. W )
Assertion	bj-fununsn2	|- ( ph -> ( F ` B ) = C )

Proof

Step	Hyp	Ref	Expression
1		bj-fununsn.un	|- ( ph -> F = ( G u. { <. B , C >. } ) )
2		bj-fununsn2.neldm	|- ( ph -> -. B e. dom G )
3		bj-fununsn2.ex1	|- ( ph -> B e. V )
4		bj-fununsn2.ex2	|- ( ph -> C e. W )
5		uncom	|- ( G u. { <. B , C >. } ) = ( { <. B , C >. } u. G )
6	1 5	eqtrdi	|- ( ph -> F = ( { <. B , C >. } u. G ) )
7	6 2	bj-funun	|- ( ph -> ( F ` B ) = ( { <. B , C >. } ` B ) )
8		fvsng	|- ( ( B e. V /\ C e. W ) -> ( { <. B , C >. } ` B ) = C )
9	3 4 8	syl2anc	|- ( ph -> ( { <. B , C >. } ` B ) = C )
10	7 9	eqtrd	|- ( ph -> ( F ` B ) = C )