| Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > ILE Home > Th. List > 2fveq3 | GIF version | ||
| Description: Equality theorem for nested function values. (Contributed by AV, 14-Aug-2022.) |
| Ref | Expression |
|---|---|
| 2fveq3 | ⊢ (𝐴 = 𝐵 → (𝐹‘(𝐺‘𝐴)) = (𝐹‘(𝐺‘𝐵))) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | fveq2 5575 | . 2 ⊢ (𝐴 = 𝐵 → (𝐺‘𝐴) = (𝐺‘𝐵)) | |
| 2 | 1 | fveq2d 5579 | 1 ⊢ (𝐴 = 𝐵 → (𝐹‘(𝐺‘𝐴)) = (𝐹‘(𝐺‘𝐵))) |
| Colors of variables: wff set class |
| Syntax hints: → wi 4 = wceq 1372 ‘cfv 5270 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-io 710 ax-5 1469 ax-7 1470 ax-gen 1471 ax-ie1 1515 ax-ie2 1516 ax-8 1526 ax-10 1527 ax-11 1528 ax-i12 1529 ax-bndl 1531 ax-4 1532 ax-17 1548 ax-i9 1552 ax-ial 1556 ax-i5r 1557 ax-ext 2186 |
| This theorem depends on definitions: df-bi 117 df-3an 982 df-tru 1375 df-nf 1483 df-sb 1785 df-clab 2191 df-cleq 2197 df-clel 2200 df-nfc 2336 df-rex 2489 df-v 2773 df-un 3169 df-sn 3638 df-pr 3639 df-op 3641 df-uni 3850 df-br 4044 df-iota 5231 df-fv 5278 |
| This theorem is referenced by: difinfsnlem 7200 ctssdclemn0 7211 cc2 7378 seq3f1olemqsum 10656 seq3f1oleml 10659 seq3f1o 10660 seq3homo 10670 seqhomog 10673 seq3coll 10985 fsumf1o 11643 iserabs 11728 explecnv 11758 cvgratnnlemnexp 11777 cvgratnnlemmn 11778 fprodf1o 11841 nninfctlemfo 12303 alginv 12311 algcvg 12312 algcvga 12315 ctiunctlemu1st 12747 ctiunctlemu2nd 12748 ctiunctlemudc 12750 ctiunctlemfo 12752 prdsbasprj 13056 prdsplusgfval 13058 prdsmulrfval 13060 prdsbas3 13061 prdsinvlem 13382 isunitd 13810 subctctexmid 15870 |
| Copyright terms: Public domain | W3C validator |