Theorem fvres 3741

Description: The value of a restricted function.

Assertion

Ref	Expression
fvres	|- (A e. B -> ((F |` B)` A) = (F` A))

Proof of Theorem fvres

Step	Hyp	Ref	Expression
1		snssi 2471	. . . . . . 7 |- (A e. B -> {A} (_ B)
2		resabs1 3395	. . . . . . 7 |- ({A} (_ B -> ((F |` B) |` {A}) = (F |` {A}))
3		rneq 3346	. . . . . . 7 |- (((F |` B) |` {A}) = (F |` {A}) -> ran ((F |` B) |` {A}) = ran ( F |` {A}))
4	1, 2, 3	3syl 20	. . . . . 6 |- (A e. B -> ran ((F |` B) |` {A}) = ran ( F |` {A}))
5		df-ima 3198	. . . . . 6 |- ((F |` B)"{A}) = ran ((F |` B) |` {A})
6		df-ima 3198	. . . . . 6 |- (F"{A}) = ran ( F |` {A})
7	4, 5, 6	3eqtr4g 1534	. . . . 5 |- (A e. B -> ((F |` B)"{A}) = (F"{A}))
8	7	eqeq1d 1486	. . . 4 |- (A e. B -> (((F |` B)"{A}) = {x} <-> (F"{A}) = {x}))
9	8	abbidv 1580	. . 3 |- (A e. B -> {x | ((F |` B)"{A}) = {x}} = {x | (F"{A}) = {x}})
10	9	unieqd 2517	. 2 |- (A e. B -> U.{x | ((F |` B)"{A}) = {x}} = U.{x | (F"{A}) = {x}})
11		df-fv 3205	. 2 |- ((F |` B)` A) = U.{x | ((F |` B)"{A}) = {x}}
12		df-fv 3205	. 2 |- (F` A) = U.{x | (F"{A}) = {x}}
13	10, 11, 12	3eqtr4g 1534	1 |- (A e. B -> ((F |` B)` A) = (F` A))

Syntax hints:   -> wi 3   = wceq 958   e. wcel 960  {cab 1466   (_ wss 2051  {csn 2414  U.cuni 2508  ran crn 3178   |` cres 3179  "cima 3180  ` cfv 3189

This theorem is referenced by:  funssfv 3742  fveqres 3756  fvsnun1 3802  fvsnun2 3803  fvreseq 3806  fnressn 3844  fressnfv 3845  fvresi 3850  funfvima 3859  abrexexlem1 3865  f1oweALT 3913  tfrlem5 3922  tz7.44-2 3936  fr0t 3959  frsuct 3960  tz7.48lem 3962  tz7.48-2 3964  oprvalres 4040  curry1 4105  df1st2 4133  df2nd2 4134  addpiord 5031  mulpiord 5032  seq1rn2 6329  seq1res 6335  shftresvalt 6353  seq0valt 6544  seqzvalt 6548  seq1seqz 6549  seq1seq0 6553  seqz1 6555  seqzp1 6556  seq00 6558  seq0p1 6559  seqzrn2 6564  seqzresval 6567  seqzres 6568  seq1ublem 6918  seq1ub 6919  fac1 6942  facp1t 6943  sumeq2 6992  climres 7112  clim2serz 7152  rescncf 7279  isupivth 7297  reeff1 7417  reeff1o 7433  reefiso 7435  unbenlem 7512  metcnss2 7903  remetdval 7912  ghsubgi 8141  sspnval 8399  efghgrpilem 8721  eff1i 8746  effoi 8747  relogclt 8761  eflogt 8762  logeft 8764  logeftb 8766  logltbt 8778  hhssnv 9136  hhssmetdval 9151

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 964  ax-gen 965  ax-8 966  ax-10 968  ax-11 969  ax-12 970  ax-13 971  ax-14 972  ax-17 973  ax-4 975  ax-5o 977  ax-6o 980  ax-9o 1125  ax-10o 1142  ax-16 1212  ax-11o 1220  ax-ext 1462  ax-sep 2709  ax-pow 2749  ax-pr 2786

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 983  df-sb 1174  df-eu 1384  df-mo 1385  df-clab 1467  df-cleq 1472  df-clel 1475  df-ne 1590  df-v 1815  df-dif 2053  df-un 2054  df-in 2055  df-ss 2057  df-nul 2285  df-pw 2407  df-sn 2417  df-pr 2418  df-op 2421  df-uni 2509  df-br 2626  df-opab 2673  df-xp 3191  df-rel 3192  df-cnv 3193  df-dm 3195  df-rn 3196  df-res 3197  df-ima 3198  df-fv 3205

Copyright terms: Public domain