![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > imbrov2fvoveq | Structured version Visualization version GIF version |
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 |
---|---|
imbrov2fvoveq.1 | โข (๐ = ๐ โ (๐ โ ๐)) |
Ref | Expression |
---|---|
imbrov2fvoveq | โข (๐ = ๐ โ ((๐ โ (๐นโ((๐บโ๐) ยท ๐))๐ ๐ด) โ (๐ โ (๐นโ((๐บโ๐) ยท ๐))๐ ๐ด))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | imbrov2fvoveq.1 | . 2 โข (๐ = ๐ โ (๐ โ ๐)) | |
2 | fveq2 6892 | . . . 4 โข (๐ = ๐ โ (๐บโ๐) = (๐บโ๐)) | |
3 | 2 | fvoveq1d 7434 | . . 3 โข (๐ = ๐ โ (๐นโ((๐บโ๐) ยท ๐)) = (๐นโ((๐บโ๐) ยท ๐))) |
4 | 3 | breq1d 5159 | . 2 โข (๐ = ๐ โ ((๐นโ((๐บโ๐) ยท ๐))๐ ๐ด โ (๐นโ((๐บโ๐) ยท ๐))๐ ๐ด)) |
5 | 1, 4 | imbi12d 343 | 1 โข (๐ = ๐ โ ((๐ โ (๐นโ((๐บโ๐) ยท ๐))๐ ๐ด) โ (๐ โ (๐นโ((๐บโ๐) ยท ๐))๐ ๐ด))) |
Colors of variables: wff setvar class |
Syntax hints: โ wi 4 โ wb 205 = wceq 1540 class class class wbr 5149 โcfv 6544 (class class class)co 7412 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1912 ax-6 1970 ax-7 2010 ax-8 2107 ax-9 2115 ax-ext 2702 |
This theorem depends on definitions: df-bi 206 df-an 396 df-or 845 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1781 df-sb 2067 df-clab 2709 df-cleq 2723 df-clel 2809 df-rab 3432 df-v 3475 df-dif 3952 df-un 3954 df-in 3956 df-ss 3966 df-nul 4324 df-if 4530 df-sn 4630 df-pr 4632 df-op 4636 df-uni 4910 df-br 5150 df-iota 6496 df-fv 6552 df-ov 7415 |
This theorem is referenced by: rlim2 15445 rlimclim1 15494 rlimcn1 15537 climcn1 15541 caucvgrlem 15624 cncfco 24648 ftc1lem4 25789 ftc1lem6 25791 itg2gt0cn 36847 ftc1cnnclem 36863 ftc1cnnc 36864 idlimc 44642 limcperiod 44644 limclner 44667 cncfshift 44890 cncfperiod 44895 fperdvper 44935 |
Copyright terms: Public domain | W3C validator |