Theorem bj-fununsn1

Description: Value of a function expressed as a union of a function and a singleton on a couple (with disjoint domain) at a point not equal to 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-fununsn1.neq	|- ( ph -> -. A = B )
Assertion	bj-fununsn1	|- ( ph -> ( F ` A ) = ( G ` A ) )

Proof

Step	Hyp	Ref	Expression
1		bj-fununsn.un	|- ( ph -> F = ( G u. { <. B , C >. } ) )
2		bj-fununsn1.neq	|- ( ph -> -. A = B )
3		dmsnopss	|- dom { <. B , C >. } C_ { B }
4	3	a1i	|- ( ph -> dom { <. B , C >. } C_ { B } )
5		elsni	|- ( A e. { B } -> A = B )
6	2 5	nsyl	|- ( ph -> -. A e. { B } )
7	4 6	ssneldd	|- ( ph -> -. A e. dom { <. B , C >. } )
8	1 7	bj-funun	|- ( ph -> ( F ` A ) = ( G ` A ) )