Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > funssfv | Structured version Visualization version GIF version |
Description: The value of a member of the domain of a subclass of a function. (Contributed by NM, 15-Aug-1994.) |
Ref | Expression |
---|---|
funssfv | ⊢ ((Fun 𝐹 ∧ 𝐺 ⊆ 𝐹 ∧ 𝐴 ∈ dom 𝐺) → (𝐹‘𝐴) = (𝐺‘𝐴)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fvres 6823 | . . . 4 ⊢ (𝐴 ∈ dom 𝐺 → ((𝐹 ↾ dom 𝐺)‘𝐴) = (𝐹‘𝐴)) | |
2 | 1 | eqcomd 2742 | . . 3 ⊢ (𝐴 ∈ dom 𝐺 → (𝐹‘𝐴) = ((𝐹 ↾ dom 𝐺)‘𝐴)) |
3 | funssres 6507 | . . . 4 ⊢ ((Fun 𝐹 ∧ 𝐺 ⊆ 𝐹) → (𝐹 ↾ dom 𝐺) = 𝐺) | |
4 | 3 | fveq1d 6806 | . . 3 ⊢ ((Fun 𝐹 ∧ 𝐺 ⊆ 𝐹) → ((𝐹 ↾ dom 𝐺)‘𝐴) = (𝐺‘𝐴)) |
5 | 2, 4 | sylan9eqr 2798 | . 2 ⊢ (((Fun 𝐹 ∧ 𝐺 ⊆ 𝐹) ∧ 𝐴 ∈ dom 𝐺) → (𝐹‘𝐴) = (𝐺‘𝐴)) |
6 | 5 | 3impa 1110 | 1 ⊢ ((Fun 𝐹 ∧ 𝐺 ⊆ 𝐹 ∧ 𝐴 ∈ dom 𝐺) → (𝐹‘𝐴) = (𝐺‘𝐴)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 397 ∧ w3a 1087 = wceq 1539 ∈ wcel 2104 ⊆ wss 3892 dom cdm 5600 ↾ cres 5602 Fun wfun 6452 ‘cfv 6458 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1911 ax-6 1969 ax-7 2009 ax-8 2106 ax-9 2114 ax-10 2135 ax-12 2169 ax-ext 2707 ax-sep 5232 ax-nul 5239 ax-pr 5361 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 846 df-3an 1089 df-tru 1542 df-fal 1552 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2538 df-eu 2567 df-clab 2714 df-cleq 2728 df-clel 2814 df-ral 3063 df-rex 3072 df-rab 3287 df-v 3439 df-dif 3895 df-un 3897 df-in 3899 df-ss 3909 df-nul 4263 df-if 4466 df-sn 4566 df-pr 4568 df-op 4572 df-uni 4845 df-br 5082 df-opab 5144 df-id 5500 df-xp 5606 df-rel 5607 df-cnv 5608 df-co 5609 df-dm 5610 df-res 5612 df-iota 6410 df-fun 6460 df-fv 6466 |
This theorem is referenced by: fviunfun 7819 funelss 7920 funsssuppss 8037 frrlem10 8142 wfrlem12OLD 8182 wfrlem14OLD 8184 tfrlem9 8247 tfrlem11 8250 ac6sfi 9102 axdc3lem2 10253 axdc3lem4 10255 imasvscaval 17294 pserdv 25633 subgruhgredgd 27696 subumgredg2 27697 subupgr 27699 sspn 29143 bnj945 32798 bnj1502 32873 bnj545 32920 bnj548 32922 subfacp1lem2a 33187 subfacp1lem2b 33188 subfacp1lem5 33191 cvmliftlem10 33301 cvmliftlem13 33303 |
Copyright terms: Public domain | W3C validator |