MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  dffun6 Structured version   Visualization version   GIF version

Theorem dffun6 5704
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
StepHypRef Expression
1 nfcv 2655 . 2 𝑥𝐹
2 nfcv 2655 . 2 𝑦𝐹
31, 2dffun6f 5703 1 (Fun 𝐹 ↔ (Rel 𝐹 ∧ ∀𝑥∃*𝑦 𝑥𝐹𝑦))
Colors of variables: wff setvar class
Syntax hints:  wb 194  wa 382  wal 1472  ∃*wmo 2363   class class class wbr 4481  Rel wrel 4937  Fun wfun 5683
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1700  ax-4 1713  ax-5 1793  ax-6 1838  ax-7 1885  ax-9 1947  ax-10 1966  ax-11 1971  ax-12 1983  ax-13 2137  ax-ext 2494  ax-sep 4607  ax-nul 4616  ax-pr 4732
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1699  df-sb 1831  df-eu 2366  df-mo 2367  df-clab 2501  df-cleq 2507  df-clel 2510  df-nfc 2644  df-ral 2805  df-rab 2809  df-v 3079  df-dif 3447  df-un 3449  df-in 3451  df-ss 3458  df-nul 3778  df-if 3940  df-sn 4029  df-pr 4031  df-op 4035  df-br 4482  df-opab 4542  df-id 4847  df-cnv 4940  df-co 4941  df-fun 5691
This theorem is referenced by:  funmo  5705  dffun7  5715  fununfun  5733  funcnvsn  5735  funcnv2  5756  svrelfun  5760  fnres  5806  nfunsn  6018  dff3  6163  brdom3  9106  nqerf  9506  shftfn  13518  cnextfun  21579  perfdvf  23349  taylf  23807
  Copyright terms: Public domain W3C validator