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 ( 𝜑𝐹 = 𝐺 )
afv2eq12d.2 ( 𝜑𝐴 = 𝐵 )
Assertion afv2eq12d ( 𝜑 → ( 𝐹 '''' 𝐴 ) = ( 𝐺 '''' 𝐵 ) )

Proof

Step Hyp Ref Expression
1 afv2eq12d.1 ( 𝜑𝐹 = 𝐺 )
2 afv2eq12d.2 ( 𝜑𝐴 = 𝐵 )
3 1 2 dfateq12d ( 𝜑 → ( 𝐹 defAt 𝐴𝐺 defAt 𝐵 ) )
4 eqidd ( 𝜑𝑥 = 𝑥 )
5 2 1 4 breq123d ( 𝜑 → ( 𝐴 𝐹 𝑥𝐵 𝐺 𝑥 ) )
6 5 iotabidv ( 𝜑 → ( ℩ 𝑥 𝐴 𝐹 𝑥 ) = ( ℩ 𝑥 𝐵 𝐺 𝑥 ) )
7 1 rneqd ( 𝜑 → ran 𝐹 = ran 𝐺 )
8 7 unieqd ( 𝜑 ran 𝐹 = ran 𝐺 )
9 8 pweqd ( 𝜑 → 𝒫 ran 𝐹 = 𝒫 ran 𝐺 )
10 3 6 9 ifbieq12d ( 𝜑 → if ( 𝐹 defAt 𝐴 , ( ℩ 𝑥 𝐴 𝐹 𝑥 ) , 𝒫 ran 𝐹 ) = if ( 𝐺 defAt 𝐵 , ( ℩ 𝑥 𝐵 𝐺 𝑥 ) , 𝒫 ran 𝐺 ) )
11 df-afv2 ( 𝐹 '''' 𝐴 ) = if ( 𝐹 defAt 𝐴 , ( ℩ 𝑥 𝐴 𝐹 𝑥 ) , 𝒫 ran 𝐹 )
12 df-afv2 ( 𝐺 '''' 𝐵 ) = if ( 𝐺 defAt 𝐵 , ( ℩ 𝑥 𝐵 𝐺 𝑥 ) , 𝒫 ran 𝐺 )
13 10 11 12 3eqtr4g ( 𝜑 → ( 𝐹 '''' 𝐴 ) = ( 𝐺 '''' 𝐵 ) )