Theorem dffn5im 5751

Description: Representation of a function in terms of its values. The converse holds given the law of the excluded middle; as it is we have most of the converse via funmpt 5418 and dmmptss 5287. (Contributed by Jim Kingdon, 31-Dec-2018.)

Assertion

Ref	Expression
dffn5im	|- ( F Fn A -> F = ( x e. A |-> ( F ` x ) ) )

Distinct variable groups:   x, A   x, F

Proof of Theorem dffn5im

Dummy variable y is distinct from all other variables.

Step	Hyp	Ref	Expression
1		fnrel 5482	. . . 4 |- ( F Fn A -> Rel F )
2		dfrel4v 5242	. . . 4 |- ( Rel F <-> F = { <. x , y >. | x F y } )
3	1, 2	sylib 122	. . 3 |- ( F Fn A -> F = { <. x , y >. | x F y } )
4		fnbr 5488	. . . . . . 7 |- ( ( F Fn A /\ x F y ) -> x e. A )
5	4	ex 115	. . . . . 6 |- ( F Fn A -> ( x F y -> x e. A ) )
6	5	pm4.71rd 398	. . . . 5 |- ( F Fn A -> ( x F y <-> ( x e. A /\ x F y ) ) )
7		eqcom 2240	. . . . . . 7 |- ( y = ( F ` x ) <-> ( F ` x ) = y )
8		fnbrfvb 5744	. . . . . . 7 |- ( ( F Fn A /\ x e. A ) -> ( ( F ` x ) = y <-> x F y ) )
9	7, 8	bitrid 192	. . . . . 6 |- ( ( F Fn A /\ x e. A ) -> ( y = ( F ` x ) <-> x F y ) )
10	9	pm5.32da 456	. . . . 5 |- ( F Fn A -> ( ( x e. A /\ y = ( F ` x ) ) <-> ( x e. A /\ x F y ) ) )
11	6, 10	bitr4d 191	. . . 4 |- ( F Fn A -> ( x F y <-> ( x e. A /\ y = ( F ` x ) ) ) )
12	11	opabbidv 4198	. . 3 |- ( F Fn A -> { <. x , y >. | x F y } = { <. x , y >. | ( x e. A /\ y = ( F ` x ) ) } )
13	3, 12	eqtrd 2271	. 2 |- ( F Fn A -> F = { <. x , y >. | ( x e. A /\ y = ( F ` x ) ) } )
14		df-mpt 4195	. 2 |- ( x e. A |-> ( F ` x ) ) = { <. x , y >. | ( x e. A /\ y = ( F ` x ) ) }
15	13, 14	eqtr4di 2289	1 |- ( F Fn A -> F = ( x e. A |-> ( F ` x ) ) )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   = wceq 1402   e. wcel 2209   class class class wbr 4131   {copab 4192   |-> cmpt 4193   Rel wrel 4781   Fn wfn 5375   ` cfv 5380

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-14 2212  ax-ext 2220  ax-sep 4251  ax-pow 4313  ax-pr 4348

This proof depends on definitions:  df-bi 117  df-3an 1011  df-tru 1405  df-nf 1514  df-sb 1816  df-eu 2089  df-mo 2090  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-ral 2533  df-rex 2534  df-v 2823  df-sbc 3052  df-un 3224  df-in 3226  df-ss 3233  df-pw 3690  df-sn 3715  df-pr 3716  df-op 3718  df-uni 3936  df-br 4132  df-opab 4194  df-mpt 4195  df-id 4440  df-xp 4782  df-rel 4783  df-cnv 4784  df-co 4785  df-dm 4786  df-iota 5340  df-fun 5382  df-fn 5383  df-fv 5388

This theorem is used by:  fnrnfv  5752  feqmptd  5759  dffn5imf  5761  eqfnfv  5809  fndmin  5819  fcompt  5881  funiun  5893  resfunexg  5939  eufnfv  5952  fnovim  6200  offveqb  6326  caofinvl  6332  oprabco  6457  df1st2  6459  df2nd2  6460  pw2f1odclem  7138  xpen  7149  prdsbascl  14296  prdsidlem  14300  prdsinvlem  14303  pws0g  14320  cnmpt1st  15514  cnmpt2nd  15515