# Metamath Proof Explorer

## Theorem afv2eq12d

Description: Equality deduction for function value, analogous to fveq12d . (Contributed by AV, 4-Sep-2022)

Ref Expression
Hypotheses afv2eq12d.1
`|- ( ph -> F = G )`
afv2eq12d.2
`|- ( ph -> A = B )`
Assertion afv2eq12d
`|- ( ph -> ( F '''' A ) = ( G '''' B ) )`

### Proof

Step Hyp Ref Expression
1 afv2eq12d.1
` |-  ( ph -> F = G )`
2 afv2eq12d.2
` |-  ( ph -> A = B )`
3 1 2 dfateq12d
` |-  ( ph -> ( F defAt A <-> G defAt B ) )`
4 eqidd
` |-  ( ph -> x = x )`
5 2 1 4 breq123d
` |-  ( ph -> ( A F x <-> B G x ) )`
6 5 iotabidv
` |-  ( ph -> ( iota x A F x ) = ( iota x B G x ) )`
7 1 rneqd
` |-  ( ph -> ran F = ran G )`
8 7 unieqd
` |-  ( ph -> U. ran F = U. ran G )`
9 8 pweqd
` |-  ( ph -> ~P U. ran F = ~P U. ran G )`
10 3 6 9 ifbieq12d
` |-  ( ph -> if ( F defAt A , ( iota x A F x ) , ~P U. ran F ) = if ( G defAt B , ( iota x B G x ) , ~P U. ran G ) )`
11 df-afv2
` |-  ( F '''' A ) = if ( F defAt A , ( iota x A F x ) , ~P U. ran F )`
12 df-afv2
` |-  ( G '''' B ) = if ( G defAt B , ( iota x B G x ) , ~P U. ran G )`
13 10 11 12 3eqtr4g
` |-  ( ph -> ( F '''' A ) = ( G '''' B ) )`