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	$$⊢\phi \to F=G\cup \left\{⟨B,C⟩\right\}$$
	bj-fununsn1.neq	$$⊢\phi \to \neg A=B$$
Assertion	bj-fununsn1	$$⊢\phi \to F\left(A\right)=G\left(A\right)$$

Proof

Step	Hyp	Ref	Expression
1		bj-fununsn.un	$$⊢\phi \to F=G\cup \left\{⟨B,C⟩\right\}$$
2		bj-fununsn1.neq	$$⊢\phi \to \neg A=B$$
3		dmsnopss	$$⊢\mathrm{dom}\left\{⟨B,C⟩\right\}\subseteq \left\{B\right\}$$
4	3	a1i	$$⊢\phi \to \mathrm{dom}\left\{⟨B,C⟩\right\}\subseteq \left\{B\right\}$$
5		elsni	$$⊢A\in \left\{B\right\}\to A=B$$
6	2 5	nsyl	$$⊢\phi \to \neg A\in \left\{B\right\}$$
7	4 6	ssneldd	$$⊢\phi \to \neg A\in \mathrm{dom}\left\{⟨B,C⟩\right\}$$
8	1 7	bj-funun	$$⊢\phi \to F\left(A\right)=G\left(A\right)$$