Theorem fvres 5141

Description: The value of a restricted function. (Contributed by NM, 2-Aug-1994.)

Assertion

Ref	Expression
fvres	⊢ (A ∈ B → ((𝐹 ↾ B)‘A) = (𝐹‘A))

Proof of Theorem fvres

Dummy variable x is distinct from all other variables.

Step	Hyp	Ref	Expression
1		vex 2554	. . . . 5 ⊢ x ∈ V
2	1	brres 4561	. . . 4 ⊢ (A(𝐹 ↾ B)x ↔ (A𝐹x ∧ A ∈ B))
3	2	rbaib 829	. . 3 ⊢ (A ∈ B → (A(𝐹 ↾ B)x ↔ A𝐹x))
4	3	iotabidv 4831	. 2 ⊢ (A ∈ B → (℩xA(𝐹 ↾ B)x) = (℩xA𝐹x))
5		df-fv 4853	. 2 ⊢ ((𝐹 ↾ B)‘A) = (℩xA(𝐹 ↾ B)x)
6		df-fv 4853	. 2 ⊢ (𝐹‘A) = (℩xA𝐹x)
7	4, 5, 6	3eqtr4g 2094	1 ⊢ (A ∈ B → ((𝐹 ↾ B)‘A) = (𝐹‘A))

Syntax hints:   → wi 4   = wceq 1242   ∈ wcel 1390   class class class wbr 3755   ↾ cres 4290  ℩cio 4808  ‘cfv 4845

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 629  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-10 1393  ax-11 1394  ax-i12 1395  ax-bndl 1396  ax-4 1397  ax-14 1402  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019  ax-sep 3866  ax-pow 3918  ax-pr 3935

This theorem depends on definitions:  df-bi 110  df-3an 886  df-tru 1245  df-nf 1347  df-sb 1643  df-clab 2024  df-cleq 2030  df-clel 2033  df-nfc 2164  df-ral 2305  df-rex 2306  df-v 2553  df-un 2916  df-in 2918  df-ss 2925  df-pw 3353  df-sn 3373  df-pr 3374  df-op 3376  df-uni 3572  df-br 3756  df-opab 3810  df-xp 4294  df-res 4300  df-iota 4810  df-fv 4853

This theorem is referenced by:  funssfv  5142  feqresmpt  5170  fvreseq  5214  respreima  5238  ffvresb  5271  fnressn  5292  fressnfv  5293  fvresi  5299  fvunsng  5300  fvsnun1  5303  fvsnun2  5304  fsnunfv  5306  funfvima  5333  isoresbr  5392  isores3  5398  isoini2  5401  ovres  5582  ofres  5667  offres  5704  fo1stresm  5730  fo2ndresm  5731  fo2ndf  5790  f1o2ndf1  5791  smores  5848  smores2  5850  tfrlem1  5864  rdgival  5909  rdgon  5913  frec0g  5922  frecsuclem1  5926  frecsuclem2  5928  frecrdg  5931  addpiord  6300  mulpiord  6301  fseq1p1m1  8726  iseqfeq2  8906