Theorem fnressn 6081

Description: A function restricted to a singleton. (Contributed by NM, 9-Oct-2004.)

Assertion

Ref	Expression
fnressn	|- ( ( F Fn A /\ B e. A ) -> ( F |` { B } ) = { <. B , ( F ` B ) >. } )

Proof of Theorem fnressn

Dummy variable x is distinct from all other variables.

Step	Hyp	Ref	Expression
1		sneq 3980	. . . . . 6 |- ( x = B -> { x } = { B } )
2	1	reseq2d 5108	. . . . 5 |- ( x = B -> ( F |` { x } ) = ( F |` { B } ) )
3		fveq2 5870	. . . . . . 7 |- ( x = B -> ( F ` x ) = ( F ` B ) )
4		opeq12 4171	. . . . . . 7 |- ( ( x = B /\ ( F ` x ) = ( F ` B ) ) -> <. x , ( F ` x ) >. = <. B , ( F ` B ) >. )
5	3, 4	mpdan 675	. . . . . 6 |- ( x = B -> <. x , ( F ` x ) >. = <. B , ( F ` B ) >. )
6	5	sneqd 3982	. . . . 5 |- ( x = B -> { <. x , ( F ` x ) >. } = { <. B , ( F ` B ) >. } )
7	2, 6	eqeq12d 2468	. . . 4 |- ( x = B -> ( ( F |` { x } ) = { <. x , ( F ` x ) >. } <-> ( F |` { B } ) = { <. B , ( F ` B ) >. } ) )
8	7	imbi2d 318	. . 3 |- ( x = B -> ( ( F Fn A -> ( F |` { x } ) = { <. x , ( F ` x ) >. } ) <-> ( F Fn A -> ( F |` { B } ) = { <. B , ( F ` B ) >. } ) ) )
9		vex 3050	. . . . . . 7 |- x e. _V
10	9	snss 4099	. . . . . 6 |- ( x e. A <-> { x } C_ A )
11		fnssres 5694	. . . . . 6 |- ( ( F Fn A /\ { x } C_ A ) -> ( F |` { x } ) Fn { x } )
12	10, 11	sylan2b 478	. . . . 5 |- ( ( F Fn A /\ x e. A ) -> ( F |` { x } ) Fn { x } )
13		dffn2 5735	. . . . . 6 |- ( ( F |` { x } ) Fn { x } <-> ( F |` { x } ) : { x } --> _V )
14	9	fsn2 6067	. . . . . 6 |- ( ( F |` { x } ) : { x } --> _V <-> ( ( ( F |` { x } ) ` x ) e. _V /\ ( F |` { x } ) = { <. x , ( ( F |` { x } ) ` x ) >. } ) )
15		fvex 5880	. . . . . . . 8 |- ( ( F |` { x } ) ` x ) e. _V
16	15	biantrur 509	. . . . . . 7 |- ( ( F |` { x } ) = { <. x , ( ( F |` { x } ) ` x ) >. } <-> ( ( ( F |` { x } ) ` x ) e. _V /\ ( F |` { x } ) = { <. x , ( ( F |` { x } ) ` x ) >. } ) )
17		ssnid 3999	. . . . . . . . . . 11 |- x e. { x }
18		fvres 5884	. . . . . . . . . . 11 |- ( x e. { x } -> ( ( F |` { x } ) ` x ) = ( F ` x ) )
19	17, 18	ax-mp 5	. . . . . . . . . 10 |- ( ( F |` { x } ) ` x ) = ( F ` x )
20	19	opeq2i 4173	. . . . . . . . 9 |- <. x , ( ( F |` { x } ) ` x ) >. = <. x , ( F ` x ) >.
21	20	sneqi 3981	. . . . . . . 8 |- { <. x , ( ( F |` { x } ) ` x ) >. } = { <. x , ( F ` x ) >. }
22	21	eqeq2i 2465	. . . . . . 7 |- ( ( F |` { x } ) = { <. x , ( ( F |` { x } ) ` x ) >. } <-> ( F |` { x } ) = { <. x , ( F ` x ) >. } )
23	16, 22	bitr3i 255	. . . . . 6 |- ( ( ( ( F |` { x } ) ` x ) e. _V /\ ( F |` { x } ) = { <. x , ( ( F |` { x } ) ` x ) >. } ) <-> ( F |` { x } ) = { <. x , ( F ` x ) >. } )
24	13, 14, 23	3bitri 275	. . . . 5 |- ( ( F |` { x } ) Fn { x } <-> ( F |` { x } ) = { <. x , ( F ` x ) >. } )
25	12, 24	sylib 200	. . . 4 |- ( ( F Fn A /\ x e. A ) -> ( F |` { x } ) = { <. x , ( F ` x ) >. } )
26	25	expcom 437	. . 3 |- ( x e. A -> ( F Fn A -> ( F |` { x } ) = { <. x , ( F ` x ) >. } ) )
27	8, 26	vtoclga 3115	. 2 |- ( B e. A -> ( F Fn A -> ( F |` { B } ) = { <. B , ( F ` B ) >. } ) )
28	27	impcom 432	1 |- ( ( F Fn A /\ B e. A ) -> ( F |` { B } ) = { <. B , ( F ` B ) >. } )

Syntax hints:   -> wi 4   /\ wa 371   = wceq 1446   e. wcel 1889   _Vcvv 3047   C_ wss 3406   {csn 3970   <.cop 3976   |` cres 4839   Fn wfn 5580   -->wf 5581   ` cfv 5585

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1671  ax-4 1684  ax-5 1760  ax-6 1807  ax-7 1853  ax-9 1898  ax-10 1917  ax-11 1922  ax-12 1935  ax-13 2093  ax-ext 2433  ax-sep 4528  ax-nul 4537  ax-pr 4642

This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 988  df-tru 1449  df-ex 1666  df-nf 1670  df-sb 1800  df-eu 2305  df-mo 2306  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2583  df-ne 2626  df-ral 2744  df-rex 2745  df-reu 2746  df-rab 2748  df-v 3049  df-sbc 3270  df-dif 3409  df-un 3411  df-in 3413  df-ss 3420  df-nul 3734  df-if 3884  df-sn 3971  df-pr 3973  df-op 3977  df-uni 4202  df-br 4406  df-opab 4465  df-id 4752  df-xp 4843  df-rel 4844  df-cnv 4845  df-co 4846  df-dm 4847  df-rn 4848  df-res 4849  df-ima 4850  df-iota 5549  df-fun 5587  df-fn 5588  df-f 5589  df-f1 5590  df-fo 5591  df-f1o 5592  df-fv 5593

This theorem is referenced by:  funressn  6082  fressnfv  6083  fnsnsplit  6106  canthp1lem2  9083  fseq1p1m1  11875  dprd2da  17687  dmdprdpr  17694  dprdpr  17695  dpjlem  17696  pgpfaclem1  17726  islindf4  19408  xpstopnlem1  20836  ptcmpfi  20840  2pthlem1  25337  eupath2lem3  25719  ginvsn  26089  subfacp1lem5  29919  cvmliftlem10  30029  poimirlem9  31961  2pthdlem1  39755