![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > mpteq12dva | Structured version Visualization version Unicode version |
Description: An equality inference for the maps to notation. (Contributed by Mario Carneiro, 26-Jan-2017.) |
Ref | Expression |
---|---|
mpteq12dv.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
mpteq12dva.2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
mpteq12dva |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mpteq12dv.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | alrimiv 1775 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | mpteq12dva.2 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 3 | ralrimiva 2804 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | mpteq12f 4482 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
6 | 2, 4, 5 | syl2anc 667 |
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 1671 ax-4 1684 ax-5 1760 ax-6 1807 ax-7 1853 ax-10 1917 ax-11 1922 ax-12 1935 ax-13 2093 ax-ext 2433 |
This theorem depends on definitions: df-bi 189 df-an 373 df-tru 1449 df-ex 1666 df-nf 1670 df-sb 1800 df-clab 2440 df-cleq 2446 df-clel 2449 df-ral 2744 df-opab 4465 df-mpt 4466 |
This theorem is referenced by: mpteq12dv 4484 reps 12880 repswccat 12895 cidpropd 15627 monpropd 15654 fucpropd 15894 curfpropd 16130 hofpropd 16164 yonffthlem 16179 ofco2 19488 pmatcollpw3fi1lem1 19822 rrxnm 22362 sgnsv 28502 ofcfval 28931 ccatmulgnn0dir 29440 signstf0 29469 cncfiooicc 37782 dvcosax 37808 fourierdlem74 38054 fourierdlem75 38055 fourierdlem93 38073 pfxmpt 38938 ushgredgedga 39316 ushgredgedgaloop 39318 |
Copyright terms: Public domain | W3C validator |