![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > mpteq2da | Structured version Unicode version |
Description: Slightly more general equality inference for the maps to notation. (Contributed by FL, 14-Sep-2013.) (Revised by Mario Carneiro, 16-Dec-2013.) |
Ref | Expression |
---|---|
mpteq2da.1 |
![]() ![]() ![]() ![]() |
mpteq2da.2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
mpteq2da |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqid 2450 |
. . 3
![]() ![]() ![]() ![]() | |
2 | 1 | ax-gen 1592 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() |
3 | mpteq2da.1 |
. . 3
![]() ![]() ![]() ![]() | |
4 | mpteq2da.2 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | 4 | ex 434 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
6 | 3, 5 | ralrimi 2879 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
7 | mpteq12f 4452 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
8 | 2, 6, 7 | sylancr 663 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1592 ax-4 1603 ax-5 1671 ax-6 1709 ax-7 1729 ax-10 1776 ax-11 1781 ax-12 1793 ax-13 1944 ax-ext 2429 |
This theorem depends on definitions: df-bi 185 df-an 371 df-tru 1373 df-ex 1588 df-nf 1591 df-sb 1702 df-clab 2436 df-cleq 2442 df-clel 2445 df-ral 2797 df-opab 4435 df-mpt 4436 |
This theorem is referenced by: mpteq2dva 4462 xkocnv 19489 utopsnneiplem 19924 offval2f 26103 fpwrelmap 26153 esumf1o 26624 prodeq1f 27541 prodeq2ii 27546 itg2addnclem 28567 ftc1anclem5 28595 mzpsubmpt 29203 mzpexpmpt 29205 refsum2cnlem1 29883 fmuldfeqlem1 29887 stoweidlem2 29921 stoweidlem6 29925 stoweidlem8 29927 stoweidlem17 29936 stoweidlem19 29938 stoweidlem20 29939 stoweidlem21 29940 stoweidlem22 29941 stoweidlem23 29942 stoweidlem32 29951 stoweidlem36 29955 stoweidlem40 29959 stoweidlem41 29960 stoweidlem47 29966 stirlinglem15 30007 gsumsndf 30887 gsummoncoe1 30971 cayleyhamilton1 31333 |
Copyright terms: Public domain | W3C validator |