Metamath Proof Explorer


Theorem imbrov2fvoveq

Description: Equality theorem for nested function and operation value in an implication for a binary relation. Technical theorem to be used to reduce the size of a significant number of proofs. (Contributed by AV, 17-Aug-2022)

Ref Expression
Hypothesis imbrov2fvoveq.1
|- ( X = Y -> ( ph <-> ps ) )
Assertion imbrov2fvoveq
|- ( X = Y -> ( ( ph -> ( F ` ( ( G ` X ) .x. O ) ) R A ) <-> ( ps -> ( F ` ( ( G ` Y ) .x. O ) ) R A ) ) )

Proof

Step Hyp Ref Expression
1 imbrov2fvoveq.1
 |-  ( X = Y -> ( ph <-> ps ) )
2 fveq2
 |-  ( X = Y -> ( G ` X ) = ( G ` Y ) )
3 2 fvoveq1d
 |-  ( X = Y -> ( F ` ( ( G ` X ) .x. O ) ) = ( F ` ( ( G ` Y ) .x. O ) ) )
4 3 breq1d
 |-  ( X = Y -> ( ( F ` ( ( G ` X ) .x. O ) ) R A <-> ( F ` ( ( G ` Y ) .x. O ) ) R A ) )
5 1 4 imbi12d
 |-  ( X = Y -> ( ( ph -> ( F ` ( ( G ` X ) .x. O ) ) R A ) <-> ( ps -> ( F ` ( ( G ` Y ) .x. O ) ) R A ) ) )