![]() |
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 5513 | . 2 ⊢ (𝐹 = 𝐺 → (𝐹‘𝐴) = (𝐺‘𝐴)) | |
3 | 1, 2 | syl 14 | 1 ⊢ (𝜑 → (𝐹‘𝐴) = (𝐺‘𝐴)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 = wceq 1353 ‘cfv 5215 |
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 709 ax-5 1447 ax-7 1448 ax-gen 1449 ax-ie1 1493 ax-ie2 1494 ax-8 1504 ax-10 1505 ax-11 1506 ax-i12 1507 ax-bndl 1509 ax-4 1510 ax-17 1526 ax-i9 1530 ax-ial 1534 ax-i5r 1535 ax-ext 2159 |
This theorem depends on definitions: df-bi 117 df-tru 1356 df-nf 1461 df-sb 1763 df-clab 2164 df-cleq 2170 df-clel 2173 df-nfc 2308 df-rex 2461 df-uni 3810 df-br 4003 df-iota 5177 df-fv 5223 |
This theorem is referenced by: fveq12d 5521 funssfv 5540 csbfv2g 5551 fvco4 5587 fvmptd 5596 fvmpt2d 5601 mpteqb 5605 fvmptt 5606 fnmptfvd 5619 fmptco 5681 fvunsng 5709 fvsng 5711 fsnunfv 5716 f1ocnvfv1 5775 f1ocnvfv2 5776 fcof1 5781 fcofo 5782 ofvalg 6089 offval2 6095 ofrfval2 6096 caofinvl 6102 tfrlemi1 6330 rdg0g 6386 freceq1 6390 oav 6452 omv 6453 oeiv 6454 mapxpen 6845 xpmapenlem 6846 nninfisollemne 7126 nninfisol 7128 exmidomni 7137 nninfwlpoimlemginf 7171 cc3 7264 fseq1p1m1 10089 seqeq3 10445 seq3f1olemqsum 10495 seq3f1olemstep 10496 seq3f1olemp 10497 seq3id 10503 seq3z 10506 exp3val 10517 bcval5 10736 bcn2 10737 seq3coll 10815 shftcan1 10836 shftcan2 10837 shftvalg 10838 shftval4g 10839 climshft2 11307 sumeq2 11360 summodc 11384 zsumdc 11385 fsum3 11388 isumz 11390 fisumss 11393 fsum3cvg2 11395 isumsplit 11492 prodeq2w 11557 prodeq2 11558 prodmodc 11579 zproddc 11580 fprodseq 11584 prod1dc 11587 fprodssdc 11591 odzval 12233 1arithlem2 12354 fvsetsid 12488 setsslid 12505 setsslnid 12506 grpinvval 12848 grpsubfvalg 12850 grpsubpropdg 12906 grpsubpropd2 12907 mulgfvalg 12917 mulgpropdg 12956 subgmulg 12979 releqgg 13011 eqgfval 13012 unitinvcl 13223 unitinvinv 13224 unitlinv 13226 unitrinv 13227 unitnegcl 13230 dvrfvald 13233 dvrvald 13234 rdivmuldivd 13244 subrgugrp 13299 ntrval 13481 clsval 13482 neival 13514 cnpval 13569 txmetcnp 13889 metcnpd 13891 limccl 13999 ellimc3apf 14000 cnplimclemr 14009 limccnp2cntop 14017 dvfvalap 14021 dvfre 14045 lgsval4 14292 lgsmod 14298 peano4nninf 14615 |
Copyright terms: Public domain | W3C validator |