Theorem bj-fvmptunsn1

Description: Value of a function expressed as a union of a mapsto expression 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-fvmptunsn.un	$$⊢\phi \to F=\left(x\in A⟼B\right)\cup \left\{⟨C,D⟩\right\}$$
	bj-fvmptunsn.nel	$$⊢\phi \to \neg C\in A$$
	bj-fvmptunsn1.ex1	$$⊢\phi \to C\in V$$
	bj-fvmptunsn1.ex2	$$⊢\phi \to D\in W$$
Assertion	bj-fvmptunsn1	$$⊢\phi \to F\left(C\right)=D$$

Proof

Step	Hyp	Ref	Expression
1		bj-fvmptunsn.un	$$⊢\phi \to F=\left(x\in A⟼B\right)\cup \left\{⟨C,D⟩\right\}$$
2		bj-fvmptunsn.nel	$$⊢\phi \to \neg C\in A$$
3		bj-fvmptunsn1.ex1	$$⊢\phi \to C\in V$$
4		bj-fvmptunsn1.ex2	$$⊢\phi \to D\in W$$
5		eqid	$$⊢\left(x\in A⟼B\right)=\left(x\in A⟼B\right)$$
6	5	dmmptss	$$⊢\mathrm{dom}\left(x\in A⟼B\right)\subseteq A$$
7	6	sseli	$$⊢C\in \mathrm{dom}\left(x\in A⟼B\right)\to C\in A$$
8	2 7	nsyl	$$⊢\phi \to \neg C\in \mathrm{dom}\left(x\in A⟼B\right)$$
9	1 8 3 4	bj-fununsn2	$$⊢\phi \to F\left(C\right)=D$$