Theorem dffun6 6152

Description: Alternate definition of a function using "at most one" notation. (Contributed by NM, 9-Mar-1995.)

Assertion

Ref	Expression
dffun6	⊢ (Fun 𝐹 ↔ (Rel 𝐹 ∧ ∀𝑥∃*𝑦 𝑥𝐹𝑦))

Distinct variable group:   𝑥,𝑦,𝐹

Proof of Theorem dffun6

Step	Hyp	Ref	Expression
1		nfcv 2934	. 2 ⊢ Ⅎ𝑥𝐹
2		nfcv 2934	. 2 ⊢ Ⅎ𝑦𝐹
3	1, 2	dffun6f 6151	1 ⊢ (Fun 𝐹 ↔ (Rel 𝐹 ∧ ∀𝑥∃*𝑦 𝑥𝐹𝑦))

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