Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > dffn2 | Structured version Visualization version Unicode version |
Description: Any function is a mapping into . (Contributed by NM, 31-Oct-1995.) (Proof shortened by Andrew Salmon, 17-Sep-2011.) |
Ref | Expression |
---|---|
dffn2 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ssv 3625 | . . 3 | |
2 | 1 | biantru 526 | . 2 |
3 | df-f 5892 | . 2 | |
4 | 2, 3 | bitr4i 267 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wb 196 wa 384 cvv 3200 wss 3574 crn 5115 wfn 5883 wf 5884 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 |
This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-clab 2609 df-cleq 2615 df-clel 2618 df-v 3202 df-in 3581 df-ss 3588 df-f 5892 |
This theorem is referenced by: f1cnvcnv 6109 fcoconst 6401 fnressn 6425 fndifnfp 6442 1stcof 7196 2ndcof 7197 fnmpt2 7238 tposfn 7381 tz7.48lem 7536 seqomlem2 7546 mptelixpg 7945 r111 8638 smobeth 9408 inar1 9597 imasvscafn 16197 fucidcl 16625 fucsect 16632 curfcl 16872 curf2ndf 16887 dsmmbas2 20081 frlmsslsp 20135 frlmup1 20137 prdstopn 21431 prdstps 21432 ist0-4 21532 ptuncnv 21610 xpstopnlem2 21614 prdstgpd 21928 prdsxmslem2 22334 curry2ima 29486 fnchoice 39188 fsneqrn 39403 stoweidlem35 40252 |
Copyright terms: Public domain | W3C validator |