Theorem fvres 5613

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 2776	. . . . 5 ⊢ 𝑥 ∈ V
2	1	brres 4974	. . . 4 ⊢ (𝐴(𝐹 ↾ 𝐵)𝑥 ↔ (𝐴𝐹𝑥 ∧ 𝐴 ∈ 𝐵))
3	2	rbaib 923	. . 3 ⊢ (𝐴 ∈ 𝐵 → (𝐴(𝐹 ↾ 𝐵)𝑥 ↔ 𝐴𝐹𝑥))
4	3	iotabidv 5263	. 2 ⊢ (𝐴 ∈ 𝐵 → (℩𝑥𝐴(𝐹 ↾ 𝐵)𝑥) = (℩𝑥𝐴𝐹𝑥))
5		df-fv 5288	. 2 ⊢ ((𝐹 ↾ 𝐵)‘𝐴) = (℩𝑥𝐴(𝐹 ↾ 𝐵)𝑥)
6		df-fv 5288	. 2 ⊢ (𝐹‘𝐴) = (℩𝑥𝐴𝐹𝑥)
7	4, 5, 6	3eqtr4g 2264	1 ⊢ (𝐴 ∈ 𝐵 → ((𝐹 ↾ 𝐵)‘𝐴) = (𝐹‘𝐴))

Syntax hints:   → wi 4   = wceq 1373   ∈ wcel 2177   class class class wbr 4051   ↾ cres 4685  ℩cio 5239  ‘cfv 5280

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 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-14 2180  ax-ext 2188  ax-sep 4170  ax-pow 4226  ax-pr 4261

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2193  df-cleq 2199  df-clel 2202  df-nfc 2338  df-ral 2490  df-rex 2491  df-v 2775  df-un 3174  df-in 3176  df-ss 3183  df-pw 3623  df-sn 3644  df-pr 3645  df-op 3647  df-uni 3857  df-br 4052  df-opab 4114  df-xp 4689  df-res 4695  df-iota 5241  df-fv 5288

This theorem is referenced by:  fvresd  5614  funssfv  5615  feqresmpt  5646  fvreseq  5696  respreima  5721  ffvresb  5756  fnressn  5783  fressnfv  5784  fvresi  5790  fvunsng  5791  fvsnun1  5794  fvsnun2  5795  fsnunfv  5798  funfvima  5829  isoresbr  5891  isores3  5897  isoini2  5901  ovres  6099  ofres  6186  offres  6233  fo1stresm  6260  fo2ndresm  6261  fo2ndf  6326  f1o2ndf1  6327  smores  6391  smores2  6393  tfrlem1  6407  rdgival  6481  frec0g  6496  freccllem  6501  frecsuclem  6505  frecrdg  6507  resixp  6833  djulclr  7166  djurclr  7167  djur  7186  updjudhcoinlf  7197  updjudhcoinrg  7198  updjud  7199  finomni  7257  exmidfodomrlemrALT  7327  addpiord  7449  mulpiord  7450  suplocexprlemell  7846  fseq1p1m1  10236  seq3feq2  10643  seqf1oglem2  10687  seq3coll  11009  pfxccat1  11178  shftidt  11219  climres  11689  fisumss  11778  isumclim3  11809  fsum2dlemstep  11820  fprodssdc  11976  fprod2dlemstep  12008  reeff1  12086  eucalgcvga  12455  eucalg  12456  strslfv2d  12950  setsslid  12958  setsslnid  12959  resmhm  13394  resghm  13671  rngmgpf  13774  mgpf  13848  znf1o  14488  cnptopresti  14785  cnptoprest  14786  lmres  14795  tx1cn  14816  tx2cn  14817  cnmpt1st  14835  cnmpt2nd  14836  remetdval  15094  rescncf  15128  limcdifap  15209  limcresi  15213  plyreres  15311  reeff1o  15320  reefiso  15324  ioocosf1o  15401  relogcl  15409  relogef  15411  logltb  15421  mpodvdsmulf1o  15537  fsumdvdsmul  15538  djucllem  15875  012of  16069  2o01f  16070