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

Theorem dffun7 5539
Description: Alternate definition of a function. One possibility for the definition of a function in [Enderton] p. 42. (Enderton's definition is ambiguous because "there is only one" could mean either "there is at most one" or "there is exactly one." However, dffun8 5540 shows that it doesn't matter which meaning we pick.) (Contributed by NM, 4-Nov-2002.)
Assertion
Ref Expression
dffun7  |-  ( Fun 
A  <->  ( Rel  A  /\  A. x  e.  dom  A E* y  x A y ) )
Distinct variable group:    x, y, A

Proof of Theorem dffun7
StepHypRef Expression
1 dffun6 5528 . 2  |-  ( Fun 
A  <->  ( Rel  A  /\  A. x E* y  x A y ) )
2 moabs 2265 . . . . . 6  |-  ( E* y  x A y  <-> 
( E. y  x A y  ->  E* y  x A y ) )
3 vex 3054 . . . . . . . 8  |-  x  e. 
_V
43eldm 5130 . . . . . . 7  |-  ( x  e.  dom  A  <->  E. y  x A y )
54imbi1i 323 . . . . . 6  |-  ( ( x  e.  dom  A  ->  E* y  x A y )  <->  ( E. y  x A y  ->  E* y  x A
y ) )
62, 5bitr4i 252 . . . . 5  |-  ( E* y  x A y  <-> 
( x  e.  dom  A  ->  E* y  x A y ) )
76albii 1655 . . . 4  |-  ( A. x E* y  x A y  <->  A. x ( x  e.  dom  A  ->  E* y  x A
y ) )
8 df-ral 2751 . . . 4  |-  ( A. x  e.  dom  A E* y  x A y  <->  A. x
( x  e.  dom  A  ->  E* y  x A y ) )
97, 8bitr4i 252 . . 3  |-  ( A. x E* y  x A y  <->  A. x  e.  dom  A E* y  x A y )
109anbi2i 692 . 2  |-  ( ( Rel  A  /\  A. x E* y  x A y )  <->  ( Rel  A  /\  A. x  e. 
dom  A E* y  x A y ) )
111, 10bitri 249 1  |-  ( Fun 
A  <->  ( Rel  A  /\  A. x  e.  dom  A E* y  x A y ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 367   A.wal 1397   E.wex 1627    e. wcel 1836   E*wmo 2233   A.wral 2746   class class class wbr 4384   dom cdm 4930   Rel wrel 4935   Fun wfun 5507
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1633  ax-4 1646  ax-5 1719  ax-6 1765  ax-7 1808  ax-9 1840  ax-10 1855  ax-11 1860  ax-12 1872  ax-13 2020  ax-ext 2374  ax-sep 4505  ax-nul 4513  ax-pr 4618
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1402  df-ex 1628  df-nf 1632  df-sb 1758  df-eu 2236  df-mo 2237  df-clab 2382  df-cleq 2388  df-clel 2391  df-nfc 2546  df-ne 2593  df-ral 2751  df-rab 2755  df-v 3053  df-dif 3409  df-un 3411  df-in 3413  df-ss 3420  df-nul 3729  df-if 3875  df-sn 3962  df-pr 3964  df-op 3968  df-br 4385  df-opab 4443  df-id 4726  df-cnv 4938  df-co 4939  df-dm 4940  df-fun 5515
This theorem is referenced by:  dffun8  5540  dffun9  5541  brdom5  8842  imasaddfnlem  14958  imasvscafn  14967  funressnfv  32418
  Copyright terms: Public domain W3C validator