ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  fvres GIF version

Theorem fvres 5313
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.
StepHypRef Expression
1 vex 2622 . . . . 5 𝑥 ∈ V
21brres 4707 . . . 4 (𝐴(𝐹𝐵)𝑥 ↔ (𝐴𝐹𝑥𝐴𝐵))
32rbaib 868 . . 3 (𝐴𝐵 → (𝐴(𝐹𝐵)𝑥𝐴𝐹𝑥))
43iotabidv 4988 . 2 (𝐴𝐵 → (℩𝑥𝐴(𝐹𝐵)𝑥) = (℩𝑥𝐴𝐹𝑥))
5 df-fv 5010 . 2 ((𝐹𝐵)‘𝐴) = (℩𝑥𝐴(𝐹𝐵)𝑥)
6 df-fv 5010 . 2 (𝐹𝐴) = (℩𝑥𝐴𝐹𝑥)
74, 5, 63eqtr4g 2145 1 (𝐴𝐵 → ((𝐹𝐵)‘𝐴) = (𝐹𝐴))
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1289  wcel 1438   class class class wbr 3837  cres 4430  cio 4965  cfv 5002
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 665  ax-5 1381  ax-7 1382  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-8 1440  ax-10 1441  ax-11 1442  ax-i12 1443  ax-bndl 1444  ax-4 1445  ax-14 1450  ax-17 1464  ax-i9 1468  ax-ial 1472  ax-i5r 1473  ax-ext 2070  ax-sep 3949  ax-pow 4001  ax-pr 4027
This theorem depends on definitions:  df-bi 115  df-3an 926  df-tru 1292  df-nf 1395  df-sb 1693  df-clab 2075  df-cleq 2081  df-clel 2084  df-nfc 2217  df-ral 2364  df-rex 2365  df-v 2621  df-un 3001  df-in 3003  df-ss 3010  df-pw 3427  df-sn 3447  df-pr 3448  df-op 3450  df-uni 3649  df-br 3838  df-opab 3892  df-xp 4434  df-res 4440  df-iota 4967  df-fv 5010
This theorem is referenced by:  funssfv  5314  feqresmpt  5342  fvreseq  5387  respreima  5411  ffvresb  5445  fnressn  5467  fressnfv  5468  fvresi  5474  fvunsng  5475  fvsnun1  5478  fvsnun2  5479  fsnunfv  5481  funfvima  5508  isoresbr  5570  isores3  5576  isoini2  5580  ovres  5766  ofres  5851  offres  5888  fo1stresm  5914  fo2ndresm  5915  fo2ndf  5974  f1o2ndf1  5975  smores  6039  smores2  6041  tfrlem1  6055  rdgival  6129  frec0g  6144  freccllem  6149  frecsuclem  6153  frecrdg  6155  djulclr  6720  djurclr  6721  updjudhcoinlf  6750  updjudhcoinrg  6751  updjud  6752  finomni  6775  exmidfodomrlemrALT  6808  addpiord  6854  mulpiord  6855  fseq1p1m1  9475  iseqfeq2  9856  seq3feq2  9858  iseqcoll  10212  shftidt  10232  climres  10655  fisumss  10748  isumclim3  10780  fsum2dlemstep  10791  eucialgcvga  11133  eucialg  11134  djucllem  11357
  Copyright terms: Public domain W3C validator