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

Theorem imbrov2fvoveq 7383
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 6843 . . . 4 (๐‘‹ = ๐‘Œ โ†’ (๐บโ€˜๐‘‹) = (๐บโ€˜๐‘Œ))
32fvoveq1d 7380 . . 3 (๐‘‹ = ๐‘Œ โ†’ (๐นโ€˜((๐บโ€˜๐‘‹) ยท ๐‘‚)) = (๐นโ€˜((๐บโ€˜๐‘Œ) ยท ๐‘‚)))
43breq1d 5116 . 2 (๐‘‹ = ๐‘Œ โ†’ ((๐นโ€˜((๐บโ€˜๐‘‹) ยท ๐‘‚))๐‘…๐ด โ†” (๐นโ€˜((๐บโ€˜๐‘Œ) ยท ๐‘‚))๐‘…๐ด))
51, 4imbi12d 345 1 (๐‘‹ = ๐‘Œ โ†’ ((๐œ‘ โ†’ (๐นโ€˜((๐บโ€˜๐‘‹) ยท ๐‘‚))๐‘…๐ด) โ†” (๐œ“ โ†’ (๐นโ€˜((๐บโ€˜๐‘Œ) ยท ๐‘‚))๐‘…๐ด)))
Colors of variables: wff setvar class
Syntax hints:   โ†’ wi 4   โ†” wb 205   = wceq 1542   class class class wbr 5106  โ€˜cfv 6497  (class class class)co 7358
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-rab 3409  df-v 3448  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4284  df-if 4488  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4867  df-br 5107  df-iota 6449  df-fv 6505  df-ov 7361
This theorem is referenced by:  rlim2  15379  rlimclim1  15428  rlimcn1  15471  climcn1  15475  caucvgrlem  15558  cncfco  24273  ftc1lem4  25406  ftc1lem6  25408  itg2gt0cn  36136  ftc1cnnclem  36152  ftc1cnnc  36153  idlimc  43874  limcperiod  43876  limclner  43899  cncfshift  44122  cncfperiod  44127  fperdvper  44167
  Copyright terms: Public domain W3C validator