![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > dprdf2 | Unicode version |
Description: The function ![]() |
Ref | Expression |
---|---|
dprdcntz.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
dprdcntz.2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
dprdf2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dprdcntz.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | dprdf 15527 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | syl 16 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | dprdcntz.2 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | 4 | feq2d 5548 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
6 | 3, 5 | mpbid 202 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() |
This theorem is referenced by: dprdff 15533 dprdfid 15538 dprdfinv 15540 dprdfadd 15541 dprdfeq0 15543 dprdres 15549 dprdss 15550 dprdf1o 15553 dprdf1 15554 subgdprd 15556 dmdprdsplitlem 15558 dprdcntz2 15559 dpjlem 15572 dpjcntz 15573 dpjdisj 15574 dpjlsm 15575 dpjf 15578 dpjidcl 15579 dpjlid 15582 dpjghm 15584 dpjghm2 15585 ablfac1c 15592 ablfac1eulem 15593 ablfac1eu 15594 ablfaclem2 15607 ablfaclem3 15608 dchrptlem3 21011 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-3 7 ax-mp 8 ax-gen 1552 ax-5 1563 ax-17 1623 ax-9 1662 ax-8 1683 ax-13 1723 ax-14 1725 ax-6 1740 ax-7 1745 ax-11 1757 ax-12 1946 ax-ext 2393 ax-rep 4288 ax-sep 4298 ax-nul 4306 ax-pow 4345 ax-pr 4371 ax-un 4668 |
This theorem depends on definitions: df-bi 178 df-or 360 df-an 361 df-3an 938 df-tru 1325 df-ex 1548 df-nf 1551 df-sb 1656 df-eu 2266 df-mo 2267 df-clab 2399 df-cleq 2405 df-clel 2408 df-nfc 2537 df-ne 2577 df-ral 2679 df-rex 2680 df-reu 2681 df-rab 2683 df-v 2926 df-sbc 3130 df-csb 3220 df-dif 3291 df-un 3293 df-in 3295 df-ss 3302 df-nul 3597 df-if 3708 df-pw 3769 df-sn 3788 df-pr 3789 df-op 3791 df-uni 3984 df-iun 4063 df-br 4181 df-opab 4235 df-mpt 4236 df-id 4466 df-xp 4851 df-rel 4852 df-cnv 4853 df-co 4854 df-dm 4855 df-rn 4856 df-res 4857 df-ima 4858 df-iota 5385 df-fun 5423 df-fn 5424 df-f 5425 df-f1 5426 df-fo 5427 df-f1o 5428 df-fv 5429 df-oprab 6052 df-mpt2 6053 df-1st 6316 df-2nd 6317 df-ixp 7031 df-dprd 15519 |
Copyright terms: Public domain | W3C validator |