![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > mpteq2dv | Unicode version |
Description: An equality inference for the maps-to notation. (Contributed by Mario Carneiro, 23-Aug-2014.) |
Ref | Expression |
---|---|
mpteq2dv.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
mpteq2dv |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mpteq2dv.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | adantr 274 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | 2 | mpteq2dva 4026 |
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: ofeq 5992 rdgeq1 6276 rdgeq2 6277 omv 6359 oeiv 6360 0tonninf 10243 1tonninf 10244 iseqf1olemjpcl 10299 iseqf1olemqpcl 10300 iseqf1olemfvp 10301 seq3f1olemqsum 10304 seq3f1olemp 10306 summodc 11184 zsumdc 11185 fsum3 11188 prodeq2w 11357 prodmodc 11379 zproddc 11380 fprodseq 11384 sloteq 12003 cnprcl2k 12414 fsumcncntop 12764 expcncf 12800 dvexp 12883 dvexp2 12884 peano4nninf 13375 peano3nninf 13376 nninfalllem1 13378 nninfsellemdc 13381 nninfsellemeq 13385 nninfsellemqall 13386 nninfsellemeqinf 13387 nninfomni 13390 |
Copyright terms: Public domain | W3C validator |