Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > fveq1d | GIF version |
Description: Equality deduction for function value. (Contributed by NM, 2-Sep-2003.) |
Ref | Expression |
---|---|
fveq1d.1 | ⊢ (𝜑 → 𝐹 = 𝐺) |
Ref | Expression |
---|---|
fveq1d | ⊢ (𝜑 → (𝐹‘𝐴) = (𝐺‘𝐴)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fveq1d.1 | . 2 ⊢ (𝜑 → 𝐹 = 𝐺) | |
2 | fveq1 5420 | . 2 ⊢ (𝐹 = 𝐺 → (𝐹‘𝐴) = (𝐺‘𝐴)) | |
3 | 1, 2 | syl 14 | 1 ⊢ (𝜑 → (𝐹‘𝐴) = (𝐺‘𝐴)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 = wceq 1331 ‘cfv 5123 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-io 698 ax-5 1423 ax-7 1424 ax-gen 1425 ax-ie1 1469 ax-ie2 1470 ax-8 1482 ax-10 1483 ax-11 1484 ax-i12 1485 ax-bndl 1486 ax-4 1487 ax-17 1506 ax-i9 1510 ax-ial 1514 ax-i5r 1515 ax-ext 2121 |
This theorem depends on definitions: df-bi 116 df-tru 1334 df-nf 1437 df-sb 1736 df-clab 2126 df-cleq 2132 df-clel 2135 df-nfc 2270 df-rex 2422 df-uni 3737 df-br 3930 df-iota 5088 df-fv 5131 |
This theorem is referenced by: fveq12d 5428 funssfv 5447 csbfv2g 5458 fvco4 5493 fvmptd 5502 fvmpt2d 5507 mpteqb 5511 fvmptt 5512 fmptco 5586 fvunsng 5614 fvsng 5616 fsnunfv 5621 f1ocnvfv1 5678 f1ocnvfv2 5679 fcof1 5684 fcofo 5685 ofvalg 5991 offval2 5997 ofrfval2 5998 caofinvl 6004 tfrlemi1 6229 rdg0g 6285 freceq1 6289 oav 6350 omv 6351 oeiv 6352 mapxpen 6742 xpmapenlem 6743 exmidomni 7014 fseq1p1m1 9874 seqeq3 10223 seq3f1olemqsum 10273 seq3f1olemstep 10274 seq3f1olemp 10275 seq3id 10281 seq3z 10284 exp3val 10295 bcval5 10509 bcn2 10510 seq3coll 10585 shftcan1 10606 shftcan2 10607 shftvalg 10608 shftval4g 10609 climshft2 11075 sumeq2 11128 summodc 11152 zsumdc 11153 fsum3 11156 isumz 11158 fisumss 11161 fsum3cvg2 11163 isumsplit 11260 prodeq2w 11325 prodeq2 11326 prodmodc 11347 fvsetsid 11993 setsslid 12009 setsslnid 12010 ntrval 12279 clsval 12280 neival 12312 cnpval 12367 txmetcnp 12687 metcnpd 12689 limccl 12797 ellimc3apf 12798 cnplimclemr 12807 limccnp2cntop 12815 dvfvalap 12819 dvfre 12843 peano4nninf 13200 |
Copyright terms: Public domain | W3C validator |