funssfv - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > funssfv		Structured version Visualization version GIF version

Theorem funssfv 6797

Description: The value of a member of the domain of a subclass of a function. (Contributed by NM, 15-Aug-1994.)

**Assertion**
Ref	Expression
funssfv	⊢ ((Fun 𝐹 ∧ 𝐺 ⊆ 𝐹 ∧ 𝐴 ∈ dom 𝐺) → (𝐹‘𝐴) = (𝐺‘𝐴))

**Proof of Theorem funssfv**
Step	Hyp	Ref	Expression
1		fvres 6795	. . . 4 ⊢ (𝐴 ∈ dom 𝐺 → ((𝐹 ↾ dom 𝐺)‘𝐴) = (𝐹‘𝐴))
2	1	eqcomd 2744	. . 3 ⊢ (𝐴 ∈ dom 𝐺 → (𝐹‘𝐴) = ((𝐹 ↾ dom 𝐺)‘𝐴))
3		funssres 6480	. . . 4 ⊢ ((Fun 𝐹 ∧ 𝐺 ⊆ 𝐹) → (𝐹 ↾ dom 𝐺) = 𝐺)
4	3	fveq1d 6778	. . 3 ⊢ ((Fun 𝐹 ∧ 𝐺 ⊆ 𝐹) → ((𝐹 ↾ dom 𝐺)‘𝐴) = (𝐺‘𝐴))
5	2, 4	sylan9eqr 2800	. 2 ⊢ (((Fun 𝐹 ∧ 𝐺 ⊆ 𝐹) ∧ 𝐴 ∈ dom 𝐺) → (𝐹‘𝐴) = (𝐺‘𝐴))
6	5	3impa 1109	1 ⊢ ((Fun 𝐹 ∧ 𝐺 ⊆ 𝐹 ∧ 𝐴 ∈ dom 𝐺) → (𝐹‘𝐴) = (𝐺‘𝐴))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 396 ∧ w3a 1086 = wceq 1539 ∈ wcel 2106 ⊆ wss 3888 dom cdm 5591 ↾ cres 5593 Fun wfun 6429 ‘cfv 6435

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2709 ax-sep 5225 ax-nul 5232 ax-pr 5354

This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1783 df-nf 1787 df-sb 2068 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2816 df-nfc 2889 df-ral 3069 df-rex 3070 df-rab 3073 df-v 3433 df-dif 3891 df-un 3893 df-in 3895 df-ss 3905 df-nul 4259 df-if 4462 df-sn 4564 df-pr 4566 df-op 4570 df-uni 4842 df-br 5077 df-opab 5139 df-id 5491 df-xp 5597 df-rel 5598 df-cnv 5599 df-co 5600 df-dm 5601 df-res 5603 df-iota 6393 df-fun 6437 df-fv 6443

This theorem is referenced by: fviunfun 7787 funelss 7888 funsssuppss 8004 frrlem10 8109 wfrlem12OLD 8149 wfrlem14OLD 8151 tfrlem9 8214 tfrlem11 8217 ac6sfi 9056 axdc3lem2 10205 axdc3lem4 10207 imasvscaval 17247 pserdv 25586 subgruhgredgd 27649 subumgredg2 27650 subupgr 27652 sspn 29095 bnj945 32750 bnj1502 32825 bnj545 32872 bnj548 32874 subfacp1lem2a 33139 subfacp1lem2b 33140 subfacp1lem5 33143 cvmliftlem10 33253 cvmliftlem13 33255