![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > fconst | Structured version Unicode version |
Description: A Cartesian product with a singleton is a constant function. (Contributed by NM, 14-Aug-1999.) (Proof shortened by Andrew Salmon, 17-Sep-2011.) |
Ref | Expression |
---|---|
fconst.1 |
![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
fconst |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fconst.1 |
. . 3
![]() ![]() ![]() ![]() | |
2 | fconstmpt 4980 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | fnmpti 5637 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | rnxpss 5368 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | df-f 5520 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
6 | 3, 4, 5 | mpbir2an 911 |
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 1592 ax-4 1603 ax-5 1671 ax-6 1710 ax-7 1730 ax-9 1762 ax-10 1777 ax-11 1782 ax-12 1794 ax-13 1952 ax-ext 2430 ax-sep 4511 ax-nul 4519 ax-pr 4629 |
This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3an 967 df-tru 1373 df-ex 1588 df-nf 1591 df-sb 1703 df-eu 2264 df-mo 2265 df-clab 2437 df-cleq 2443 df-clel 2446 df-nfc 2601 df-ne 2646 df-ral 2800 df-rex 2801 df-rab 2804 df-v 3070 df-dif 3429 df-un 3431 df-in 3433 df-ss 3440 df-nul 3736 df-if 3890 df-sn 3976 df-pr 3978 df-op 3982 df-br 4391 df-opab 4449 df-mpt 4450 df-id 4734 df-xp 4944 df-rel 4945 df-cnv 4946 df-co 4947 df-dm 4948 df-rn 4949 df-fun 5518 df-fn 5519 df-f 5520 |
This theorem is referenced by: fconstg 5695 fodomr 7562 ofsubeq0 10420 ser0f 11960 hashgval 12207 hashinf 12209 hashf 12211 pwssplit1 17246 psrbag0 17683 xkofvcn 19373 ibl0 21380 dvcmul 21534 dvcmulf 21535 dvexp 21543 elqaalem3 21903 basellem7 22540 basellem9 22542 axlowdimlem8 23330 axlowdimlem9 23331 axlowdimlem10 23332 axlowdimlem11 23333 axlowdimlem12 23334 0oo 24324 occllem 24841 ho01i 25367 nlelchi 25600 hmopidmchi 25690 eulerpartlemt 26888 plymul02 27081 prodf1f 27541 fullfunfnv 28111 fullfunfv 28112 ftc1anclem5 28609 diophrw 29235 pwssplit4 29580 ofsubid 29736 dvsconst 29742 dvsid 29743 lfl0f 33020 |
Copyright terms: Public domain | W3C validator |