# 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 ${⊢}{\phi }\to {F}={G}$
afv2eq12d.2 ${⊢}{\phi }\to {A}={B}$
Assertion afv2eq12d ${⊢}{\phi }\to \left({F}\mathrm{\text{'}\text{'}\text{'}\text{'}}{A}\right)=\left({G}\mathrm{\text{'}\text{'}\text{'}\text{'}}{B}\right)$

### Proof

Step Hyp Ref Expression
1 afv2eq12d.1 ${⊢}{\phi }\to {F}={G}$
2 afv2eq12d.2 ${⊢}{\phi }\to {A}={B}$
3 1 2 dfateq12d ${⊢}{\phi }\to \left({F}\mathrm{defAt}{A}↔{G}\mathrm{defAt}{B}\right)$
4 eqidd ${⊢}{\phi }\to {x}={x}$
5 2 1 4 breq123d ${⊢}{\phi }\to \left({A}{F}{x}↔{B}{G}{x}\right)$
6 5 iotabidv ${⊢}{\phi }\to \left(\iota {x}|{A}{F}{x}\right)=\left(\iota {x}|{B}{G}{x}\right)$
7 1 rneqd ${⊢}{\phi }\to \mathrm{ran}{F}=\mathrm{ran}{G}$
8 7 unieqd ${⊢}{\phi }\to \bigcup \mathrm{ran}{F}=\bigcup \mathrm{ran}{G}$
9 8 pweqd ${⊢}{\phi }\to 𝒫\bigcup \mathrm{ran}{F}=𝒫\bigcup \mathrm{ran}{G}$
10 3 6 9 ifbieq12d ${⊢}{\phi }\to if\left({F}\mathrm{defAt}{A},\left(\iota {x}|{A}{F}{x}\right),𝒫\bigcup \mathrm{ran}{F}\right)=if\left({G}\mathrm{defAt}{B},\left(\iota {x}|{B}{G}{x}\right),𝒫\bigcup \mathrm{ran}{G}\right)$
11 df-afv2 ${⊢}\left({F}\mathrm{\text{'}\text{'}\text{'}\text{'}}{A}\right)=if\left({F}\mathrm{defAt}{A},\left(\iota {x}|{A}{F}{x}\right),𝒫\bigcup \mathrm{ran}{F}\right)$
12 df-afv2 ${⊢}\left({G}\mathrm{\text{'}\text{'}\text{'}\text{'}}{B}\right)=if\left({G}\mathrm{defAt}{B},\left(\iota {x}|{B}{G}{x}\right),𝒫\bigcup \mathrm{ran}{G}\right)$
13 10 11 12 3eqtr4g ${⊢}{\phi }\to \left({F}\mathrm{\text{'}\text{'}\text{'}\text{'}}{A}\right)=\left({G}\mathrm{\text{'}\text{'}\text{'}\text{'}}{B}\right)$