Theorem fniniseg2

Description: Inverse point images under functions expressed as abstractions. (Contributed by Stefan O'Rear, 1-Feb-2015)

	Ref	Expression
Assertion	fniniseg2	⊢ ( 𝐹 Fn 𝐴 → ( ◡ 𝐹 “ { 𝐵 } ) = { 𝑥 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑥 ) = 𝐵 } )

Proof

Step	Hyp	Ref	Expression
1		fncnvima2	⊢ ( 𝐹 Fn 𝐴 → ( ◡ 𝐹 “ { 𝐵 } ) = { 𝑥 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑥 ) ∈ { 𝐵 } } )
2		fvex	⊢ ( 𝐹 ‘ 𝑥 ) ∈ V
3	2	elsn	⊢ ( ( 𝐹 ‘ 𝑥 ) ∈ { 𝐵 } ↔ ( 𝐹 ‘ 𝑥 ) = 𝐵 )
4	3	rabbii	⊢ { 𝑥 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑥 ) ∈ { 𝐵 } } = { 𝑥 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑥 ) = 𝐵 }
5	1 4	eqtrdi	⊢ ( 𝐹 Fn 𝐴 → ( ◡ 𝐹 “ { 𝐵 } ) = { 𝑥 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑥 ) = 𝐵 } )