Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > fveq1d | Unicode 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 5493 | . 2 | |
3 | 1, 2 | syl 14 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wceq 1348 cfv 5196 |
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 704 ax-5 1440 ax-7 1441 ax-gen 1442 ax-ie1 1486 ax-ie2 1487 ax-8 1497 ax-10 1498 ax-11 1499 ax-i12 1500 ax-bndl 1502 ax-4 1503 ax-17 1519 ax-i9 1523 ax-ial 1527 ax-i5r 1528 ax-ext 2152 |
This theorem depends on definitions: df-bi 116 df-tru 1351 df-nf 1454 df-sb 1756 df-clab 2157 df-cleq 2163 df-clel 2166 df-nfc 2301 df-rex 2454 df-uni 3795 df-br 3988 df-iota 5158 df-fv 5204 |
This theorem is referenced by: fveq12d 5501 funssfv 5520 csbfv2g 5531 fvco4 5566 fvmptd 5575 fvmpt2d 5580 mpteqb 5584 fvmptt 5585 fnmptfvd 5598 fmptco 5660 fvunsng 5688 fvsng 5690 fsnunfv 5695 f1ocnvfv1 5754 f1ocnvfv2 5755 fcof1 5760 fcofo 5761 ofvalg 6068 offval2 6074 ofrfval2 6075 caofinvl 6081 tfrlemi1 6309 rdg0g 6365 freceq1 6369 oav 6431 omv 6432 oeiv 6433 mapxpen 6824 xpmapenlem 6825 nninfisollemne 7105 nninfisol 7107 exmidomni 7116 cc3 7223 fseq1p1m1 10043 seqeq3 10399 seq3f1olemqsum 10449 seq3f1olemstep 10450 seq3f1olemp 10451 seq3id 10457 seq3z 10460 exp3val 10471 bcval5 10690 bcn2 10691 seq3coll 10770 shftcan1 10791 shftcan2 10792 shftvalg 10793 shftval4g 10794 climshft2 11262 sumeq2 11315 summodc 11339 zsumdc 11340 fsum3 11343 isumz 11345 fisumss 11348 fsum3cvg2 11350 isumsplit 11447 prodeq2w 11512 prodeq2 11513 prodmodc 11534 zproddc 11535 fprodseq 11539 prod1dc 11542 fprodssdc 11546 odzval 12188 1arithlem2 12309 fvsetsid 12443 setsslid 12459 setsslnid 12460 ntrval 12869 clsval 12870 neival 12902 cnpval 12957 txmetcnp 13277 metcnpd 13279 limccl 13387 ellimc3apf 13388 cnplimclemr 13397 limccnp2cntop 13405 dvfvalap 13409 dvfre 13433 lgsval4 13680 lgsmod 13686 peano4nninf 14004 |
Copyright terms: Public domain | W3C validator |