![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > mpt2eq123dv | Structured version Visualization version Unicode version |
Description: An equality deduction for the maps to notation. (Contributed by NM, 12-Sep-2011.) |
Ref | Expression |
---|---|
mpt2eq123dv.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
mpt2eq123dv.2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
mpt2eq123dv.3 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
mpt2eq123dv |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mpt2eq123dv.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | mpt2eq123dv.2 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 2 | adantr 467 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | mpt2eq123dv.3 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | 4 | adantr 467 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
6 | 1, 3, 5 | mpt2eq123dva 6349 |
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 1668 ax-4 1681 ax-5 1757 ax-6 1804 ax-7 1850 ax-10 1914 ax-11 1919 ax-12 1932 ax-13 2090 ax-ext 2430 |
This theorem depends on definitions: df-bi 189 df-an 373 df-tru 1446 df-ex 1663 df-nf 1667 df-sb 1797 df-clab 2437 df-cleq 2443 df-clel 2446 df-oprab 6292 df-mpt2 6293 |
This theorem is referenced by: mpt2eq123i 6351 bropopvvv 6871 bropfvvvv 6873 prdsval 15346 imasval 15404 imasvalOLD 15405 imasvscaval 15437 homffval 15588 homfeq 15592 comfffval 15596 comffval 15597 comfffval2 15599 comffval2 15600 comfeq 15604 oppcval 15611 monfval 15630 sectffval 15648 invffval 15656 isofn 15673 cofuval 15780 natfval 15844 fucval 15856 fucco 15860 coafval 15952 setcval 15965 setcco 15971 catcval 15984 catcco 15989 estrcval 16002 estrcco 16008 xpcval 16055 xpchomfval 16057 xpccofval 16060 1stfval 16069 2ndfval 16072 prfval 16077 evlfval 16095 evlf2 16096 curfval 16101 hofval 16130 hof2fval 16133 plusffval 16486 grpsubfval 16701 grpsubpropd 16749 mulgfval 16752 mulgpropd 16784 symgval 17013 lsmfval 17283 pj1fval 17337 efgtf 17365 prdsmgp 17831 dvrfval 17905 scaffval 18102 psrval 18579 ipffval 19208 frlmip 19329 mamufval 19403 mvmulfval 19560 marrepfval 19578 marepvfval 19583 submafval 19597 submaval 19599 madufval 19655 minmar1fval 19664 mat2pmatfval 19740 cpm2mfval 19766 decpmatval0 19781 decpmatval 19782 pmatcollpw3lem 19800 xkoval 20595 xkopt 20663 xpstopnlem1 20817 submtmd 21112 blfvalps 21391 ishtpy 21996 isphtpy 22005 pcofval 22034 rrxip 22342 q1pval 23097 r1pval 23100 taylfval 23307 midf 24811 ismidb 24813 ttgval 24898 wlkon 25254 trlon 25263 pthon 25298 spthon 25305 is2wlkonot 25584 is2spthonot 25585 2wlkonot3v 25596 2spthonot3v 25597 grpodivfval 25963 gxfval 25978 dipfval 26331 submatres 28625 lmatval 28632 lmatcl 28635 qqhval 28771 sxval 29005 sitmval 29175 cndprobval 29259 mclsval 30194 csbfinxpg 31773 rrnval 32152 ldualset 32685 paddfval 33356 tgrpfset 34305 tgrpset 34306 erngfset 34360 erngset 34361 erngfset-rN 34368 erngset-rN 34369 dvafset 34565 dvaset 34566 dvhfset 34642 dvhset 34643 djaffvalN 34695 djafvalN 34696 djhffval 34958 djhfval 34959 hlhilset 35499 eldiophb 35593 mendval 36043 hoidmvval 38393 ovnhoi 38419 hspval 38425 hspmbllem2 38443 hoimbl 38447 wlkson 39640 rngcvalALTV 39950 rngccoALTV 39977 funcrngcsetcALT 39988 ringcvalALTV 39996 ringccoALTV 40040 lincop 40188 |
Copyright terms: Public domain | W3C validator |