![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > dffun6 | Structured version Visualization version GIF version |
Description: Alternate definition of a function using "at most one" notation. (Contributed by NM, 9-Mar-1995.) |
Ref | Expression |
---|---|
dffun6 | ⊢ (Fun 𝐹 ↔ (Rel 𝐹 ∧ ∀𝑥∃*𝑦 𝑥𝐹𝑦)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfcv 2934 | . 2 ⊢ Ⅎ𝑥𝐹 | |
2 | nfcv 2934 | . 2 ⊢ Ⅎ𝑦𝐹 | |
3 | 1, 2 | dffun6f 6151 | 1 ⊢ (Fun 𝐹 ↔ (Rel 𝐹 ∧ ∀𝑥∃*𝑦 𝑥𝐹𝑦)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 198 ∧ wa 386 ∀wal 1599 ∃*wmo 2549 class class class wbr 4888 Rel wrel 5362 Fun wfun 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-13 2334 ax-ext 2754 ax-sep 5019 ax-nul 5027 ax-pr 5140 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 837 df-3an 1073 df-tru 1605 df-ex 1824 df-nf 1828 df-sb 2012 df-mo 2551 df-eu 2587 df-clab 2764 df-cleq 2770 df-clel 2774 df-nfc 2921 df-ral 3095 df-rab 3099 df-v 3400 df-dif 3795 df-un 3797 df-in 3799 df-ss 3806 df-nul 4142 df-if 4308 df-sn 4399 df-pr 4401 df-op 4405 df-br 4889 df-opab 4951 df-id 5263 df-cnv 5365 df-co 5366 df-fun 6139 |
This theorem is referenced by: funmo 6153 dffun7 6164 fununfun 6184 funcnvsn 6186 funcnv2 6204 svrelfun 6208 fnres 6255 nfunsn 6486 dff3 6638 brdom3 9687 nqerf 10089 shftfn 14224 cnextfun 22280 perfdvf 24108 taylf 24556 funressnvmo 42119 funressnvmoOLD 42120 |
Copyright terms: Public domain | W3C validator |