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

Theorem dffun6 5615
Description: Alternate definition of a function using "at most one" notation. (Contributed by NM, 9-Mar-1995.)
Assertion
Ref Expression
dffun6  |-  ( Fun 
F  <->  ( Rel  F  /\  A. x E* y  x F y ) )
Distinct variable group:    x, y, F

Proof of Theorem dffun6
StepHypRef Expression
1 nfcv 2602 . 2  |-  F/_ x F
2 nfcv 2602 . 2  |-  F/_ y F
31, 2dffun6f 5614 1  |-  ( Fun 
F  <->  ( Rel  F  /\  A. x E* y  x F y ) )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 189    /\ wa 375   A.wal 1452   E*wmo 2310   class class class wbr 4415   Rel wrel 4857   Fun wfun 5594
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-6 1815  ax-7 1861  ax-9 1906  ax-10 1925  ax-11 1930  ax-12 1943  ax-13 2101  ax-ext 2441  ax-sep 4538  ax-nul 4547  ax-pr 4652
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3an 993  df-tru 1457  df-ex 1674  df-nf 1678  df-sb 1808  df-eu 2313  df-mo 2314  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2591  df-ne 2634  df-ral 2753  df-rab 2757  df-v 3058  df-dif 3418  df-un 3420  df-in 3422  df-ss 3429  df-nul 3743  df-if 3893  df-sn 3980  df-pr 3982  df-op 3986  df-br 4416  df-opab 4475  df-id 4767  df-cnv 4860  df-co 4861  df-fun 5602
This theorem is referenced by:  funmo  5616  dffun7  5626  fununfun  5644  funcnvsn  5645  funcnv2  5663  svrelfun  5667  fnres  5713  nfunsn  5918  dff3  6057  brdom3  8981  nqerf  9380  shftfn  13184  cnextfun  21127  perfdvf  22906  taylf  23364
  Copyright terms: Public domain W3C validator