![]() |
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 271 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | 2 | mpteq2dva 3950 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-5 1388 ax-7 1389 ax-gen 1390 ax-ie1 1434 ax-ie2 1435 ax-8 1447 ax-11 1449 ax-4 1452 ax-17 1471 ax-i9 1475 ax-ial 1479 ax-i5r 1480 ax-ext 2077 |
This theorem depends on definitions: df-bi 116 df-tru 1299 df-nf 1402 df-sb 1700 df-clab 2082 df-cleq 2088 df-clel 2091 df-ral 2375 df-opab 3922 df-mpt 3923 |
This theorem is referenced by: ofeq 5896 rdgeq1 6174 rdgeq2 6175 omv 6256 oeiv 6257 0tonninf 9994 1tonninf 9995 iseqf1olemjpcl 10061 iseqf1olemqpcl 10062 iseqf1olemfvp 10063 seq3f1olemqsum 10066 seq3f1olemp 10068 summodc 10941 zsumdc 10942 fsum3 10945 sloteq 11663 cnprcl2k 12072 peano4nninf 12605 peano3nninf 12606 nninfalllem1 12608 nninfsellemdc 12611 nninfsellemeq 12615 nninfsellemqall 12616 nninfsellemeqinf 12617 nninfomni 12620 |
Copyright terms: Public domain | W3C validator |