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	$$⊢\phi \to F=G\cup \left\{⟨B,C⟩\right\}$$
	bj-fununsn2.neldm	$$⊢\phi \to \neg B\in \mathrm{dom}G$$
	bj-fununsn2.ex1	$$⊢\phi \to B\in V$$
	bj-fununsn2.ex2	$$⊢\phi \to C\in W$$
Assertion	bj-fununsn2	$$⊢\phi \to F\left(B\right)=C$$

Proof

Step	Hyp	Ref	Expression
1		bj-fununsn.un	$$⊢\phi \to F=G\cup \left\{⟨B,C⟩\right\}$$
2		bj-fununsn2.neldm	$$⊢\phi \to \neg B\in \mathrm{dom}G$$
3		bj-fununsn2.ex1	$$⊢\phi \to B\in V$$
4		bj-fununsn2.ex2	$$⊢\phi \to C\in W$$
5		uncom	$$⊢G\cup \left\{⟨B,C⟩\right\}=\left\{⟨B,C⟩\right\}\cup G$$
6	1 5	eqtrdi	$$⊢\phi \to F=\left\{⟨B,C⟩\right\}\cup G$$
7	6 2	bj-funun	$$⊢\phi \to F\left(B\right)=\left\{⟨B,C⟩\right\}\left(B\right)$$
8		fvsng	$$⊢\left(B\in V\wedge C\in W\right)\to \left\{⟨B,C⟩\right\}\left(B\right)=C$$
9	3 4 8	syl2anc	$$⊢\phi \to \left\{⟨B,C⟩\right\}\left(B\right)=C$$
10	7 9	eqtrd	$$⊢\phi \to F\left(B\right)=C$$