Theorem fvimacnvi

Description: A member of a preimage is a function value argument. (Contributed by NM, 4-May-2007)

	Ref	Expression
Assertion	fvimacnvi	⊢ ( ( Fun 𝐹 ∧ 𝐴 ∈ ( ◡ 𝐹 “ 𝐵 ) ) → ( 𝐹 ‘ 𝐴 ) ∈ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		snssi	⊢ ( 𝐴 ∈ ( ◡ 𝐹 “ 𝐵 ) → { 𝐴 } ⊆ ( ◡ 𝐹 “ 𝐵 ) )
2		funimass2	⊢ ( ( Fun 𝐹 ∧ { 𝐴 } ⊆ ( ◡ 𝐹 “ 𝐵 ) ) → ( 𝐹 “ { 𝐴 } ) ⊆ 𝐵 )
3	1 2	sylan2	⊢ ( ( Fun 𝐹 ∧ 𝐴 ∈ ( ◡ 𝐹 “ 𝐵 ) ) → ( 𝐹 “ { 𝐴 } ) ⊆ 𝐵 )
4		fvex	⊢ ( 𝐹 ‘ 𝐴 ) ∈ V
5	4	snss	⊢ ( ( 𝐹 ‘ 𝐴 ) ∈ 𝐵 ↔ { ( 𝐹 ‘ 𝐴 ) } ⊆ 𝐵 )
6		cnvimass	⊢ ( ◡ 𝐹 “ 𝐵 ) ⊆ dom 𝐹
7	6	sseli	⊢ ( 𝐴 ∈ ( ◡ 𝐹 “ 𝐵 ) → 𝐴 ∈ dom 𝐹 )
8		funfn	⊢ ( Fun 𝐹 ↔ 𝐹 Fn dom 𝐹 )
9		fnsnfv	⊢ ( ( 𝐹 Fn dom 𝐹 ∧ 𝐴 ∈ dom 𝐹 ) → { ( 𝐹 ‘ 𝐴 ) } = ( 𝐹 “ { 𝐴 } ) )
10	8 9	sylanb	⊢ ( ( Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹 ) → { ( 𝐹 ‘ 𝐴 ) } = ( 𝐹 “ { 𝐴 } ) )
11	7 10	sylan2	⊢ ( ( Fun 𝐹 ∧ 𝐴 ∈ ( ◡ 𝐹 “ 𝐵 ) ) → { ( 𝐹 ‘ 𝐴 ) } = ( 𝐹 “ { 𝐴 } ) )
12	11	sseq1d	⊢ ( ( Fun 𝐹 ∧ 𝐴 ∈ ( ◡ 𝐹 “ 𝐵 ) ) → ( { ( 𝐹 ‘ 𝐴 ) } ⊆ 𝐵 ↔ ( 𝐹 “ { 𝐴 } ) ⊆ 𝐵 ) )
13	5 12	bitrid	⊢ ( ( Fun 𝐹 ∧ 𝐴 ∈ ( ◡ 𝐹 “ 𝐵 ) ) → ( ( 𝐹 ‘ 𝐴 ) ∈ 𝐵 ↔ ( 𝐹 “ { 𝐴 } ) ⊆ 𝐵 ) )
14	3 13	mpbird	⊢ ( ( Fun 𝐹 ∧ 𝐴 ∈ ( ◡ 𝐹 “ 𝐵 ) ) → ( 𝐹 ‘ 𝐴 ) ∈ 𝐵 )