Metamath Proof Explorer


Theorem bj-fvsnun2

Description: The value of a function with one of its ordered pairs replaced, at the replaced ordered pair. See also fvsnun2 . (Contributed by NM, 23-Sep-2007) Put in deduction form. (Revised by BJ, 18-Mar-2023) (Proof modification is discouraged.)

Ref Expression
Hypotheses bj-fvsnun.un φ G = F C A A B
bj-fvsnun2.ex1 φ A V
bj-fvsnun2.ex2 φ B W
Assertion bj-fvsnun2 φ G A = B

Proof

Step Hyp Ref Expression
1 bj-fvsnun.un φ G = F C A A B
2 bj-fvsnun2.ex1 φ A V
3 bj-fvsnun2.ex2 φ B W
4 dmres dom F C A = C A dom F
5 inss1 C A dom F C A
6 4 5 eqsstri dom F C A C A
7 6 a1i φ dom F C A C A
8 neldifsnd φ ¬ A C A
9 7 8 ssneldd φ ¬ A dom F C A
10 1 9 2 3 bj-fununsn2 φ G A = B