Theorem funfvima3

Description: A class including a function contains the function's value in the image of the singleton of the argument. (Contributed by NM, 23-Mar-2004)

	Ref	Expression
Assertion	funfvima3	⊢ ( ( Fun 𝐹 ∧ 𝐹 ⊆ 𝐺 ) → ( 𝐴 ∈ dom 𝐹 → ( 𝐹 ‘ 𝐴 ) ∈ ( 𝐺 “ { 𝐴 } ) ) )

Proof

Step	Hyp	Ref	Expression
1		ssel	⊢ ( 𝐹 ⊆ 𝐺 → ( ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ ∈ 𝐹 → ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ ∈ 𝐺 ) )
2		funfvop	⊢ ( ( Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹 ) → ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ ∈ 𝐹 )
3	1 2	impel	⊢ ( ( 𝐹 ⊆ 𝐺 ∧ ( Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹 ) ) → ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ ∈ 𝐺 )
4		sneq	⊢ ( 𝑥 = 𝐴 → { 𝑥 } = { 𝐴 } )
5	4	imaeq2d	⊢ ( 𝑥 = 𝐴 → ( 𝐺 “ { 𝑥 } ) = ( 𝐺 “ { 𝐴 } ) )
6	5	eleq2d	⊢ ( 𝑥 = 𝐴 → ( ( 𝐹 ‘ 𝐴 ) ∈ ( 𝐺 “ { 𝑥 } ) ↔ ( 𝐹 ‘ 𝐴 ) ∈ ( 𝐺 “ { 𝐴 } ) ) )
7		opeq1	⊢ ( 𝑥 = 𝐴 → ⟨ 𝑥 , ( 𝐹 ‘ 𝐴 ) ⟩ = ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ )
8	7	eleq1d	⊢ ( 𝑥 = 𝐴 → ( ⟨ 𝑥 , ( 𝐹 ‘ 𝐴 ) ⟩ ∈ 𝐺 ↔ ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ ∈ 𝐺 ) )
9		vex	⊢ 𝑥 ∈ V
10		fvex	⊢ ( 𝐹 ‘ 𝐴 ) ∈ V
11	9 10	elimasn	⊢ ( ( 𝐹 ‘ 𝐴 ) ∈ ( 𝐺 “ { 𝑥 } ) ↔ ⟨ 𝑥 , ( 𝐹 ‘ 𝐴 ) ⟩ ∈ 𝐺 )
12	6 8 11	vtoclbg	⊢ ( 𝐴 ∈ dom 𝐹 → ( ( 𝐹 ‘ 𝐴 ) ∈ ( 𝐺 “ { 𝐴 } ) ↔ ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ ∈ 𝐺 ) )
13	12	ad2antll	⊢ ( ( 𝐹 ⊆ 𝐺 ∧ ( Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹 ) ) → ( ( 𝐹 ‘ 𝐴 ) ∈ ( 𝐺 “ { 𝐴 } ) ↔ ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ ∈ 𝐺 ) )
14	3 13	mpbird	⊢ ( ( 𝐹 ⊆ 𝐺 ∧ ( Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹 ) ) → ( 𝐹 ‘ 𝐴 ) ∈ ( 𝐺 “ { 𝐴 } ) )
15	14	exp32	⊢ ( 𝐹 ⊆ 𝐺 → ( Fun 𝐹 → ( 𝐴 ∈ dom 𝐹 → ( 𝐹 ‘ 𝐴 ) ∈ ( 𝐺 “ { 𝐴 } ) ) ) )
16	15	impcom	⊢ ( ( Fun 𝐹 ∧ 𝐹 ⊆ 𝐺 ) → ( 𝐴 ∈ dom 𝐹 → ( 𝐹 ‘ 𝐴 ) ∈ ( 𝐺 “ { 𝐴 } ) ) )