Metamath Proof Explorer


Theorem bj-funun

Description: Value of a function expressed as a union of two functions at a point not in the domain of one of them. (Contributed by BJ, 18-Mar-2023)

Ref Expression
Hypotheses bj-funun.un φ F = G H
bj-funun.neldm φ ¬ A dom H
Assertion bj-funun φ F A = G A

Proof

Step Hyp Ref Expression
1 bj-funun.un φ F = G H
2 bj-funun.neldm φ ¬ A dom H
3 imaeq1 F = G H F A = G H A
4 imaundir G H A = G A H A
5 3 4 eqtrdi F = G H F A = G A H A
6 1 5 syl φ F A = G A H A
7 ndmima ¬ A dom H H A =
8 2 7 syl φ H A =
9 uneq2 H A = G A H A = G A
10 un0 G A = G A
11 9 10 eqtrdi H A = G A H A = G A
12 8 11 syl φ G A H A = G A
13 6 12 eqtrd φ F A = G A
14 bj-imafv F A = G A F A = G A
15 13 14 syl φ F A = G A