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

Theorem imbrov2fvoveq 7444
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 6885 . . . 4 (𝑋 = 𝑌 → (𝐺𝑋) = (𝐺𝑌))
32fvoveq1d 7441 . . 3 (𝑋 = 𝑌 → (𝐹‘((𝐺𝑋) · 𝑂)) = (𝐹‘((𝐺𝑌) · 𝑂)))
43breq1d 5121 . 2 (𝑋 = 𝑌 → ((𝐹‘((𝐺𝑋) · 𝑂))𝑅𝐴 ↔ (𝐹‘((𝐺𝑌) · 𝑂))𝑅𝐴))
51, 4imbi12d 347 1 (𝑋 = 𝑌 → ((𝜑 → (𝐹‘((𝐺𝑋) · 𝑂))𝑅𝐴) ↔ (𝜓 → (𝐹‘((𝐺𝑌) · 𝑂))𝑅𝐴)))
Colors of variables:    wff setvar class
This proof depends on syntax axioms:  wi 4  wb 209   = wceq 1570   class class class wbr 5111  cfv 6540  (class class class)co 7419
This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737
This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-iota 6496  df-fv 6548  df-ov 7422
This theorem is used by:  rlim2  15573  rlimclim1  15622  rlimcn1  15665  climcn1  15669  caucvgrlem  15750  cncfco  25119  ftc1lem4  26251  ftc1lem6  26253  itg2gt0cn  38385  ftc1cnnclem  38401  ftc1cnnc  38402  idlimc  46402  limcperiod  46404  limclner  46425  cncfshift  46648  cncfperiod  46653  fperdvper  46693
  Copyright terms: Public domain W3C validator