![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > dffn2 | Structured version Visualization version GIF version |
Description: Any function is a mapping into V. (Contributed by NM, 31-Oct-1995.) (Proof shortened by Andrew Salmon, 17-Sep-2011.) |
Ref | Expression |
---|---|
dffn2 | ⊢ (𝐹 Fn 𝐴 ↔ 𝐹:𝐴⟶V) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ssv 4004 | . . 3 ⊢ ran 𝐹 ⊆ V | |
2 | 1 | biantru 528 | . 2 ⊢ (𝐹 Fn 𝐴 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ V)) |
3 | df-f 6548 | . 2 ⊢ (𝐹:𝐴⟶V ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ V)) | |
4 | 2, 3 | bitr4i 277 | 1 ⊢ (𝐹 Fn 𝐴 ↔ 𝐹:𝐴⟶V) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 205 ∧ wa 394 Vcvv 3463 ⊆ wss 3947 ran crn 5674 Fn wfn 6539 ⟶wf 6540 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-ext 2697 |
This theorem depends on definitions: df-bi 206 df-an 395 df-tru 1537 df-ex 1775 df-sb 2061 df-clab 2704 df-cleq 2718 df-clel 2803 df-v 3465 df-ss 3964 df-f 6548 |
This theorem is referenced by: f1cnvcnv 6797 fcoconst 7138 fnressn 7162 fndifnfp 7180 1stcof 8023 2ndcof 8024 fnmpo 8073 tposfn 8260 tz7.48lem 8461 seqomlem2 8471 mptelixpg 8954 r111 9809 smobeth 10618 inar1 10807 imasvscafn 17545 fucidcl 17983 fucsect 17990 dfinito3 18020 dftermo3 18021 curfcl 18250 curf2ndf 18265 dsmmbas2 21729 frlmsslsp 21788 frlmup1 21790 prdstopn 23618 prdstps 23619 ist0-4 23719 ptuncnv 23797 xpstopnlem2 23801 prdstgpd 24115 prdsxmslem2 24524 curry2ima 32618 fnchoice 44663 fsneqrn 44852 stoweidlem35 45690 |
Copyright terms: Public domain | W3C validator |