Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  imbrov2fvoveq Structured version   Visualization version   GIF version

Theorem imbrov2fvoveq 7181
 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.)
Hypothesis
Ref Expression
imbrov2fvoveq.1 (𝑋 = 𝑌 → (𝜑𝜓))
Assertion
Ref Expression
imbrov2fvoveq (𝑋 = 𝑌 → ((𝜑 → (𝐹‘((𝐺𝑋) · 𝑂))𝑅𝐴) ↔ (𝜓 → (𝐹‘((𝐺𝑌) · 𝑂))𝑅𝐴)))

Proof of Theorem imbrov2fvoveq
StepHypRef Expression
1 imbrov2fvoveq.1 . 2 (𝑋 = 𝑌 → (𝜑𝜓))
2 fveq2 6663 . . . 4 (𝑋 = 𝑌 → (𝐺𝑋) = (𝐺𝑌))
32fvoveq1d 7178 . . 3 (𝑋 = 𝑌 → (𝐹‘((𝐺𝑋) · 𝑂)) = (𝐹‘((𝐺𝑌) · 𝑂)))
43breq1d 5046 . 2 (𝑋 = 𝑌 → ((𝐹‘((𝐺𝑋) · 𝑂))𝑅𝐴 ↔ (𝐹‘((𝐺𝑌) · 𝑂))𝑅𝐴))
51, 4imbi12d 348 1 (𝑋 = 𝑌 → ((𝜑 → (𝐹‘((𝐺𝑋) · 𝑂))𝑅𝐴) ↔ (𝜓 → (𝐹‘((𝐺𝑌) · 𝑂))𝑅𝐴)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   = wceq 1538   class class class wbr 5036  ‘cfv 6340  (class class class)co 7156 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2729 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2736  df-cleq 2750  df-clel 2830  df-v 3411  df-un 3865  df-in 3867  df-ss 3877  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4802  df-br 5037  df-iota 6299  df-fv 6348  df-ov 7159 This theorem is referenced by:  rlim2  14914  rlimclim1  14963  rlimcn1  15006  climcn1  15009  caucvgrlem  15090  cncfco  23621  ftc1lem4  24751  ftc1lem6  24753  itg2gt0cn  35426  ftc1cnnclem  35442  ftc1cnnc  35443  idlimc  42669  limcperiod  42671  limclner  42694  cncfshift  42917  cncfperiod  42922  fperdvper  42962
 Copyright terms: Public domain W3C validator