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 2663 | . . . . 5 ⊢ 𝑥 ∈ V | |
2 | 1 | brres 4795 | . . . 4 ⊢ (𝐴(𝐹 ↾ 𝐵)𝑥 ↔ (𝐴𝐹𝑥 ∧ 𝐴 ∈ 𝐵)) |
3 | 2 | rbaib 891 | . . 3 ⊢ (𝐴 ∈ 𝐵 → (𝐴(𝐹 ↾ 𝐵)𝑥 ↔ 𝐴𝐹𝑥)) |
4 | 3 | iotabidv 5079 | . 2 ⊢ (𝐴 ∈ 𝐵 → (℩𝑥𝐴(𝐹 ↾ 𝐵)𝑥) = (℩𝑥𝐴𝐹𝑥)) |
5 | df-fv 5101 | . 2 ⊢ ((𝐹 ↾ 𝐵)‘𝐴) = (℩𝑥𝐴(𝐹 ↾ 𝐵)𝑥) | |
6 | df-fv 5101 | . 2 ⊢ (𝐹‘𝐴) = (℩𝑥𝐴𝐹𝑥) | |
7 | 4, 5, 6 | 3eqtr4g 2175 | 1 ⊢ (𝐴 ∈ 𝐵 → ((𝐹 ↾ 𝐵)‘𝐴) = (𝐹‘𝐴)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 = wceq 1316 ∈ wcel 1465 class class class wbr 3899 ↾ cres 4511 ℩cio 5056 ‘cfv 5093 |
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 683 ax-5 1408 ax-7 1409 ax-gen 1410 ax-ie1 1454 ax-ie2 1455 ax-8 1467 ax-10 1468 ax-11 1469 ax-i12 1470 ax-bndl 1471 ax-4 1472 ax-14 1477 ax-17 1491 ax-i9 1495 ax-ial 1499 ax-i5r 1500 ax-ext 2099 ax-sep 4016 ax-pow 4068 ax-pr 4101 |
This theorem depends on definitions: df-bi 116 df-3an 949 df-tru 1319 df-nf 1422 df-sb 1721 df-clab 2104 df-cleq 2110 df-clel 2113 df-nfc 2247 df-ral 2398 df-rex 2399 df-v 2662 df-un 3045 df-in 3047 df-ss 3054 df-pw 3482 df-sn 3503 df-pr 3504 df-op 3506 df-uni 3707 df-br 3900 df-opab 3960 df-xp 4515 df-res 4521 df-iota 5058 df-fv 5101 |
This theorem is referenced by: fvresd 5414 funssfv 5415 feqresmpt 5443 fvreseq 5492 respreima 5516 ffvresb 5551 fnressn 5574 fressnfv 5575 fvresi 5581 fvunsng 5582 fvsnun1 5585 fvsnun2 5586 fsnunfv 5589 funfvima 5617 isoresbr 5678 isores3 5684 isoini2 5688 ovres 5878 ofres 5964 offres 6001 fo1stresm 6027 fo2ndresm 6028 fo2ndf 6092 f1o2ndf1 6093 smores 6157 smores2 6159 tfrlem1 6173 rdgival 6247 frec0g 6262 freccllem 6267 frecsuclem 6271 frecrdg 6273 resixp 6595 djulclr 6902 djurclr 6903 djur 6922 updjudhcoinlf 6933 updjudhcoinrg 6934 updjud 6935 finomni 6980 exmidfodomrlemrALT 7027 addpiord 7092 mulpiord 7093 suplocexprlemell 7489 fseq1p1m1 9842 seq3feq2 10211 seq3coll 10553 shftidt 10573 climres 11040 fisumss 11129 isumclim3 11160 fsum2dlemstep 11171 reeff1 11334 eucalgcvga 11666 eucalg 11667 strslfv2d 11928 setsslid 11936 setsslnid 11937 cnptopresti 12334 cnptoprest 12335 lmres 12344 tx1cn 12365 tx2cn 12366 cnmpt1st 12384 cnmpt2nd 12385 remetdval 12635 rescncf 12664 limcdifap 12727 limcresi 12731 djucllem 12934 isomninnlem 13152 |
Copyright terms: Public domain | W3C validator |