Theorem fvres 5672

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 2806	. . . . 5 ⊢ 𝑥 ∈ V
2	1	brres 5025	. . . 4 ⊢ (𝐴(𝐹 ↾ 𝐵)𝑥 ↔ (𝐴𝐹𝑥 ∧ 𝐴 ∈ 𝐵))
3	2	rbaib 929	. . 3 ⊢ (𝐴 ∈ 𝐵 → (𝐴(𝐹 ↾ 𝐵)𝑥 ↔ 𝐴𝐹𝑥))
4	3	iotabidv 5316	. 2 ⊢ (𝐴 ∈ 𝐵 → (℩𝑥𝐴(𝐹 ↾ 𝐵)𝑥) = (℩𝑥𝐴𝐹𝑥))
5		df-fv 5341	. 2 ⊢ ((𝐹 ↾ 𝐵)‘𝐴) = (℩𝑥𝐴(𝐹 ↾ 𝐵)𝑥)
6		df-fv 5341	. 2 ⊢ (𝐹‘𝐴) = (℩𝑥𝐴𝐹𝑥)
7	4, 5, 6	3eqtr4g 2289	1 ⊢ (𝐴 ∈ 𝐵 → ((𝐹 ↾ 𝐵)‘𝐴) = (𝐹‘𝐴))

Syntax hints:   → wi 4   = wceq 1398   ∈ wcel 2202   class class class wbr 4093   ↾ cres 4733  ℩cio 5291  ‘cfv 5333

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-14 2205  ax-ext 2213  ax-sep 4212  ax-pow 4270  ax-pr 4305

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2364  df-ral 2516  df-rex 2517  df-v 2805  df-un 3205  df-in 3207  df-ss 3214  df-pw 3658  df-sn 3679  df-pr 3680  df-op 3682  df-uni 3899  df-br 4094  df-opab 4156  df-xp 4737  df-res 4743  df-iota 5293  df-fv 5341

This theorem is referenced by:  fvresd  5673  funssfv  5674  feqresmpt  5709  fvreseq  5759  respreima  5783  ffvresb  5818  fnressn  5848  fressnfv  5849  fvresi  5855  fvunsng  5856  fvsnun1  5859  fvsnun2  5860  fsnunfv  5863  funfvima  5896  isoresbr  5960  isores3  5966  isoini2  5970  ovres  6172  ofres  6259  offres  6306  fo1stresm  6333  fo2ndresm  6334  fo2ndf  6401  f1o2ndf1  6402  smores  6501  smores2  6503  tfrlem1  6517  rdgival  6591  frec0g  6606  freccllem  6611  frecsuclem  6615  frecrdg  6617  resixp  6945  djulclr  7291  djurclr  7292  djur  7311  updjudhcoinlf  7322  updjudhcoinrg  7323  updjud  7324  finomni  7382  exmidfodomrlemrALT  7457  addpiord  7579  mulpiord  7580  suplocexprlemell  7976  fseq1p1m1  10374  seq3feq2  10784  seqf1oglem2  10828  seq3coll  11152  pfxccat1  11332  shftidt  11456  climres  11926  fisumss  12016  isumclim3  12047  fsum2dlemstep  12058  fprodssdc  12214  fprod2dlemstep  12246  reeff1  12324  eucalgcvga  12693  eucalg  12694  strslfv2d  13188  setsslid  13196  setsslnid  13197  resmhm  13633  resghm  13910  rngmgpf  14014  mgpf  14088  znf1o  14730  cnptopresti  15032  cnptoprest  15033  lmres  15042  tx1cn  15063  tx2cn  15064  cnmpt1st  15082  cnmpt2nd  15083  remetdval  15341  rescncf  15375  limcdifap  15456  limcresi  15460  plyreres  15558  reeff1o  15567  reefiso  15571  ioocosf1o  15648  relogcl  15656  relogef  15658  logltb  15668  mpodvdsmulf1o  15787  fsumdvdsmul  15788  djucllem  16501  012of  16696  2o01f  16697