Metamath Proof Explorer


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 φ F = G B C
bj-fununsn2.neldm φ ¬ B dom G
bj-fununsn2.ex1 φ B V
bj-fununsn2.ex2 φ C W
Assertion bj-fununsn2 φ F B = C

Proof

Step Hyp Ref Expression
1 bj-fununsn.un φ F = G B C
2 bj-fununsn2.neldm φ ¬ B dom G
3 bj-fununsn2.ex1 φ B V
4 bj-fununsn2.ex2 φ C W
5 uncom G B C = B C G
6 1 5 eqtrdi φ F = B C G
7 6 2 bj-funun φ F B = B C B
8 fvsng B V C W B C B = C
9 3 4 8 syl2anc φ B C B = C
10 7 9 eqtrd φ F B = C