![]() |
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 3973 | . . 3 ⊢ ran 𝐹 ⊆ V | |
2 | 1 | biantru 531 | . 2 ⊢ (𝐹 Fn 𝐴 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ V)) |
3 | df-f 6505 | . 2 ⊢ (𝐹:𝐴⟶V ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ V)) | |
4 | 2, 3 | bitr4i 278 | 1 ⊢ (𝐹 Fn 𝐴 ↔ 𝐹:𝐴⟶V) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 205 ∧ wa 397 Vcvv 3448 ⊆ wss 3915 ran crn 5639 Fn wfn 6496 ⟶wf 6497 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-ext 2708 |
This theorem depends on definitions: df-bi 206 df-an 398 df-tru 1545 df-ex 1783 df-sb 2069 df-clab 2715 df-cleq 2729 df-clel 2815 df-v 3450 df-in 3922 df-ss 3932 df-f 6505 |
This theorem is referenced by: f1cnvcnv 6753 fcoconst 7085 fnressn 7109 fndifnfp 7127 1stcof 7956 2ndcof 7957 fnmpo 8006 tposfn 8191 tz7.48lem 8392 seqomlem2 8402 mptelixpg 8880 r111 9718 smobeth 10529 inar1 10718 imasvscafn 17426 fucidcl 17861 fucsect 17868 dfinito3 17898 dftermo3 17899 curfcl 18128 curf2ndf 18143 dsmmbas2 21159 frlmsslsp 21218 frlmup1 21220 prdstopn 22995 prdstps 22996 ist0-4 23096 ptuncnv 23174 xpstopnlem2 23178 prdstgpd 23492 prdsxmslem2 23901 curry2ima 31664 fnchoice 43308 fsneqrn 43506 stoweidlem35 44350 |
Copyright terms: Public domain | W3C validator |