![]() |
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 3844 | . . 3 ⊢ ran 𝐹 ⊆ V | |
2 | 1 | biantru 525 | . 2 ⊢ (𝐹 Fn 𝐴 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ V)) |
3 | df-f 6139 | . 2 ⊢ (𝐹:𝐴⟶V ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ V)) | |
4 | 2, 3 | bitr4i 270 | 1 ⊢ (𝐹 Fn 𝐴 ↔ 𝐹:𝐴⟶V) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 198 ∧ wa 386 Vcvv 3398 ⊆ wss 3792 ran crn 5356 Fn wfn 6130 ⟶wf 6131 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1839 ax-4 1853 ax-5 1953 ax-6 2021 ax-7 2055 ax-9 2116 ax-10 2135 ax-11 2150 ax-12 2163 ax-ext 2754 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 837 df-tru 1605 df-ex 1824 df-nf 1828 df-sb 2012 df-clab 2764 df-cleq 2770 df-clel 2774 df-v 3400 df-in 3799 df-ss 3806 df-f 6139 |
This theorem is referenced by: f1cnvcnv 6360 fcoconst 6666 fnressn 6691 fndifnfp 6709 1stcof 7475 2ndcof 7476 fnmpt2 7518 tposfn 7663 tz7.48lem 7819 seqomlem2 7829 mptelixpg 8231 r111 8935 smobeth 9743 inar1 9932 imasvscafn 16583 fucidcl 17010 fucsect 17017 curfcl 17258 curf2ndf 17273 dsmmbas2 20480 frlmsslsp 20539 frlmup1 20541 prdstopn 21840 prdstps 21841 ist0-4 21941 ptuncnv 22019 xpstopnlem2 22023 prdstgpd 22336 prdsxmslem2 22742 curry2ima 30052 fnchoice 40121 fsneqrn 40324 stoweidlem35 41179 |
Copyright terms: Public domain | W3C validator |