| 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 1551 |
. 2
| |
| 2 | mpteq2dva.1 |
. 2
| |
| 3 | 1, 2 | mpteq2da 4133 |
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 106 ax-ia2 107 ax-ia3 108 ax-5 1470 ax-7 1471 ax-gen 1472 ax-ie1 1516 ax-ie2 1517 ax-8 1527 ax-11 1529 ax-4 1533 ax-17 1549 ax-i9 1553 ax-ial 1557 ax-i5r 1558 ax-ext 2187 |
| This theorem depends on definitions: df-bi 117 df-tru 1376 df-nf 1484 df-sb 1786 df-clab 2192 df-cleq 2198 df-clel 2201 df-ral 2489 df-opab 4106 df-mpt 4107 |
| This theorem is referenced by: mpteq2dv 4135 fmptapd 5775 offval 6166 offval2 6174 caofinvl 6184 caofcom 6189 caofdig 6192 freceq1 6478 freceq2 6479 pw2f1odclem 6931 mapxpen 6945 xpmapenlem 6946 nnnninf2 7229 nninfwlpoimlemginf 7278 fser0const 10680 sumeq1 11666 sumeq2 11670 prodeq2 11868 prod1dc 11897 restid2 13080 pwsplusgval 13127 pwsmulrval 13128 qusin 13158 prdssgrpd 13247 prdsidlem 13279 prdsmndd 13280 grpinvpropdg 13407 prdsinvlem 13440 pwsinvg 13444 pwssub 13445 mulgrhm2 14372 psrlinv 14446 cnmpt1t 14757 cnmpt12 14759 fsumcncntop 15039 expcn 15041 divccncfap 15062 cdivcncfap 15076 expcncf 15081 divcncfap 15086 maxcncf 15087 mincncf 15088 dvidlemap 15163 dvidrelem 15164 dvidsslem 15165 dvcnp2cntop 15171 dvaddxxbr 15173 dvmulxxbr 15174 dvimulf 15178 dvcoapbr 15179 dvcjbr 15180 dvcj 15181 dvfre 15182 dvexp 15183 dvexp2 15184 dvrecap 15185 dvmptcmulcn 15193 dvmptnegcn 15194 dvmptsubcn 15195 dvmptfsum 15197 dvef 15199 ply1termlem 15214 plypow 15216 plyconst 15217 plyaddlem1 15219 plymullem1 15220 plycolemc 15230 plycjlemc 15232 dvply1 15237 dvply2g 15238 lgsval4lem 15488 lgsneg 15501 lgsmod 15503 lgseisenlem3 15549 lgseisenlem4 15550 2omap 15932 |
| Copyright terms: Public domain | W3C validator |