Theorem fvres 5453

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

Assertion

Ref	Expression
fvres	⊢ (𝐴 ∈ 𝐵 → ((𝐹 ↾ 𝐵)‘𝐴) = (𝐹‘𝐴))

Proof of Theorem fvres

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		vex 2692	. . . . 5 ⊢ 𝑥 ∈ V
2	1	brres 4833	. . . 4 ⊢ (𝐴(𝐹 ↾ 𝐵)𝑥 ↔ (𝐴𝐹𝑥 ∧ 𝐴 ∈ 𝐵))
3	2	rbaib 907	. . 3 ⊢ (𝐴 ∈ 𝐵 → (𝐴(𝐹 ↾ 𝐵)𝑥 ↔ 𝐴𝐹𝑥))
4	3	iotabidv 5117	. 2 ⊢ (𝐴 ∈ 𝐵 → (℩𝑥𝐴(𝐹 ↾ 𝐵)𝑥) = (℩𝑥𝐴𝐹𝑥))
5		df-fv 5139	. 2 ⊢ ((𝐹 ↾ 𝐵)‘𝐴) = (℩𝑥𝐴(𝐹 ↾ 𝐵)𝑥)
6		df-fv 5139	. 2 ⊢ (𝐹‘𝐴) = (℩𝑥𝐴𝐹𝑥)
7	4, 5, 6	3eqtr4g 2198	1 ⊢ (𝐴 ∈ 𝐵 → ((𝐹 ↾ 𝐵)‘𝐴) = (𝐹‘𝐴))

Syntax hints:   → wi 4   = wceq 1332   ∈ wcel 1481   class class class wbr 3937   ↾ cres 4549  ℩cio 5094  ‘cfv 5131

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-14 1493  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122  ax-sep 4054  ax-pow 4106  ax-pr 4139

This theorem depends on definitions:  df-bi 116  df-3an 965  df-tru 1335  df-nf 1438  df-sb 1737  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-ral 2422  df-rex 2423  df-v 2691  df-un 3080  df-in 3082  df-ss 3089  df-pw 3517  df-sn 3538  df-pr 3539  df-op 3541  df-uni 3745  df-br 3938  df-opab 3998  df-xp 4553  df-res 4559  df-iota 5096  df-fv 5139

This theorem is referenced by:  fvresd  5454  funssfv  5455  feqresmpt  5483  fvreseq  5532  respreima  5556  ffvresb  5591  fnressn  5614  fressnfv  5615  fvresi  5621  fvunsng  5622  fvsnun1  5625  fvsnun2  5626  fsnunfv  5629  funfvima  5657  isoresbr  5718  isores3  5724  isoini2  5728  ovres  5918  ofres  6004  offres  6041  fo1stresm  6067  fo2ndresm  6068  fo2ndf  6132  f1o2ndf1  6133  smores  6197  smores2  6199  tfrlem1  6213  rdgival  6287  frec0g  6302  freccllem  6307  frecsuclem  6311  frecrdg  6313  resixp  6635  djulclr  6942  djurclr  6943  djur  6962  updjudhcoinlf  6973  updjudhcoinrg  6974  updjud  6975  finomni  7020  exmidfodomrlemrALT  7076  addpiord  7148  mulpiord  7149  suplocexprlemell  7545  fseq1p1m1  9905  seq3feq2  10274  seq3coll  10617  shftidt  10637  climres  11104  fisumss  11193  isumclim3  11224  fsum2dlemstep  11235  reeff1  11443  eucalgcvga  11775  eucalg  11776  strslfv2d  12040  setsslid  12048  setsslnid  12049  cnptopresti  12446  cnptoprest  12447  lmres  12456  tx1cn  12477  tx2cn  12478  cnmpt1st  12496  cnmpt2nd  12497  remetdval  12747  rescncf  12776  limcdifap  12839  limcresi  12843  reeff1o  12902  reefiso  12906  ioocosf1o  12983  relogcl  12991  relogef  12993  logltb  13003  djucllem  13178  012of  13363  2o01f  13364