![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > fvres | GIF version |
Description: The value of a restricted function. (Contributed by NM, 2-Aug-1994.) |
Ref | Expression |
---|---|
fvres | ⊢ (𝐴 ∈ 𝐵 → ((𝐹 ↾ 𝐵)‘𝐴) = (𝐹‘𝐴)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | vex 2615 | . . . . 5 ⊢ 𝑥 ∈ V | |
2 | 1 | brres 4677 | . . . 4 ⊢ (𝐴(𝐹 ↾ 𝐵)𝑥 ↔ (𝐴𝐹𝑥 ∧ 𝐴 ∈ 𝐵)) |
3 | 2 | rbaib 864 | . . 3 ⊢ (𝐴 ∈ 𝐵 → (𝐴(𝐹 ↾ 𝐵)𝑥 ↔ 𝐴𝐹𝑥)) |
4 | 3 | iotabidv 4955 | . 2 ⊢ (𝐴 ∈ 𝐵 → (℩𝑥𝐴(𝐹 ↾ 𝐵)𝑥) = (℩𝑥𝐴𝐹𝑥)) |
5 | df-fv 4977 | . 2 ⊢ ((𝐹 ↾ 𝐵)‘𝐴) = (℩𝑥𝐴(𝐹 ↾ 𝐵)𝑥) | |
6 | df-fv 4977 | . 2 ⊢ (𝐹‘𝐴) = (℩𝑥𝐴𝐹𝑥) | |
7 | 4, 5, 6 | 3eqtr4g 2140 | 1 ⊢ (𝐴 ∈ 𝐵 → ((𝐹 ↾ 𝐵)‘𝐴) = (𝐹‘𝐴)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 = wceq 1285 ∈ wcel 1434 class class class wbr 3811 ↾ cres 4403 ℩cio 4932 ‘cfv 4969 |
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 663 ax-5 1377 ax-7 1378 ax-gen 1379 ax-ie1 1423 ax-ie2 1424 ax-8 1436 ax-10 1437 ax-11 1438 ax-i12 1439 ax-bndl 1440 ax-4 1441 ax-14 1446 ax-17 1460 ax-i9 1464 ax-ial 1468 ax-i5r 1469 ax-ext 2065 ax-sep 3922 ax-pow 3974 ax-pr 4000 |
This theorem depends on definitions: df-bi 115 df-3an 922 df-tru 1288 df-nf 1391 df-sb 1688 df-clab 2070 df-cleq 2076 df-clel 2079 df-nfc 2212 df-ral 2358 df-rex 2359 df-v 2614 df-un 2988 df-in 2990 df-ss 2997 df-pw 3408 df-sn 3428 df-pr 3429 df-op 3431 df-uni 3628 df-br 3812 df-opab 3866 df-xp 4407 df-res 4413 df-iota 4934 df-fv 4977 |
This theorem is referenced by: funssfv 5275 feqresmpt 5303 fvreseq 5348 respreima 5372 ffvresb 5403 fnressn 5425 fressnfv 5426 fvresi 5432 fvunsng 5433 fvsnun1 5436 fvsnun2 5437 fsnunfv 5439 funfvima 5466 isoresbr 5528 isores3 5534 isoini2 5537 ovres 5719 ofres 5804 offres 5841 fo1stresm 5867 fo2ndresm 5868 fo2ndf 5927 f1o2ndf1 5928 smores 5989 smores2 5991 tfrlem1 6005 rdgival 6079 frec0g 6094 freccllem 6099 frecsuclem 6103 frecrdg 6105 djulclr 6648 djurclr 6649 updjudhcoinlf 6678 updjudhcoinrg 6679 updjud 6680 finomni 6701 exmidfodomrlemrALT 6732 addpiord 6778 mulpiord 6779 fseq1p1m1 9401 iseqfeq2 9764 shftidt 10095 climres 10516 eucialgcvga 10820 eucialg 10821 djucllem 11043 |
Copyright terms: Public domain | W3C validator |