![]() |
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 1509 |
. 2
![]() ![]() ![]() ![]() | |
2 | mpteq2dva.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | mpteq2da 4025 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() |
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 1424 ax-7 1425 ax-gen 1426 ax-ie1 1470 ax-ie2 1471 ax-8 1483 ax-11 1485 ax-4 1488 ax-17 1507 ax-i9 1511 ax-ial 1515 ax-i5r 1516 ax-ext 2122 |
This theorem depends on definitions: df-bi 116 df-tru 1335 df-nf 1438 df-sb 1737 df-clab 2127 df-cleq 2133 df-clel 2136 df-ral 2422 df-opab 3998 df-mpt 3999 |
This theorem is referenced by: mpteq2dv 4027 fmptapd 5619 offval 5997 offval2 6005 caofinvl 6012 caofcom 6013 freceq1 6297 freceq2 6298 mapxpen 6750 xpmapenlem 6751 fser0const 10320 sumeq1 11156 sumeq2 11160 prodeq2 11358 restid2 12168 cnmpt1t 12493 cnmpt12 12495 fsumcncntop 12764 divccncfap 12785 cdivcncfap 12795 expcncf 12800 dvidlemap 12868 dvcnp2cntop 12871 dvaddxxbr 12873 dvmulxxbr 12874 dvimulf 12878 dvcoapbr 12879 dvcjbr 12880 dvcj 12881 dvfre 12882 dvexp 12883 dvexp2 12884 dvrecap 12885 dvmptcmulcn 12891 dvmptnegcn 12892 dvmptsubcn 12893 dvef 12896 |
Copyright terms: Public domain | W3C validator |