Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > mpteq2dva | Unicode version |
Description: Slightly more general equality inference for the maps-to notation. (Contributed by Scott Fenton, 25-Apr-2012.) |
Ref | Expression |
---|---|
mpteq2dva.1 |
Ref | Expression |
---|---|
mpteq2dva |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfv 1521 | . 2 | |
2 | mpteq2dva.1 | . 2 | |
3 | 1, 2 | mpteq2da 4076 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 103 wceq 1348 wcel 2141 cmpt 4048 |
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-5 1440 ax-7 1441 ax-gen 1442 ax-ie1 1486 ax-ie2 1487 ax-8 1497 ax-11 1499 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-ral 2453 df-opab 4049 df-mpt 4050 |
This theorem is referenced by: mpteq2dv 4078 fmptapd 5684 offval 6065 offval2 6073 caofinvl 6080 caofcom 6081 freceq1 6368 freceq2 6369 mapxpen 6822 xpmapenlem 6823 nnnninf2 7099 fser0const 10459 sumeq1 11305 sumeq2 11309 prodeq2 11507 prod1dc 11536 restid2 12574 cnmpt1t 13000 cnmpt12 13002 fsumcncntop 13271 divccncfap 13292 cdivcncfap 13302 expcncf 13307 dvidlemap 13375 dvcnp2cntop 13378 dvaddxxbr 13380 dvmulxxbr 13381 dvimulf 13385 dvcoapbr 13386 dvcjbr 13387 dvcj 13388 dvfre 13389 dvexp 13390 dvexp2 13391 dvrecap 13392 dvmptcmulcn 13398 dvmptnegcn 13399 dvmptsubcn 13400 dvef 13403 lgsval4lem 13627 lgsneg 13640 lgsmod 13642 |
Copyright terms: Public domain | W3C validator |