Theorem bj-fvmptunsn2

Description: Value of a function expressed as a union of a mapsto expression and a singleton on a couple (with disjoint domain) at a point in the domain of the mapsto construction. (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-fvmptunsn2.el	$$⊢\phi \to E\in A$$
	bj-fvmptunsn2.ex	$$⊢\phi \to G\in V$$
	bj-fvmptunsn2.is	$$⊢\left(\phi \wedge x=E\right)\to B=G$$
Assertion	bj-fvmptunsn2	$$⊢\phi \to F\left(E\right)=G$$

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-fvmptunsn2.el	$$⊢\phi \to E\in A$$
4		bj-fvmptunsn2.ex	$$⊢\phi \to G\in V$$
5		bj-fvmptunsn2.is	$$⊢\left(\phi \wedge x=E\right)\to B=G$$
6		nelneq	$$⊢\left(E\in A\wedge \neg C\in A\right)\to \neg E=C$$
7	3 2 6	syl2anc	$$⊢\phi \to \neg E=C$$
8	1 7	bj-fununsn1	$$⊢\phi \to F\left(E\right)=\left(x\in A⟼B\right)\left(E\right)$$
9		eqidd	$$⊢\phi \to \left(x\in A⟼B\right)=\left(x\in A⟼B\right)$$
10	9 5 3 4	fvmptd	$$⊢\phi \to \left(x\in A⟼B\right)\left(E\right)=G$$
11	8 10	eqtrd	$$⊢\phi \to F\left(E\right)=G$$