Metamath Proof Explorer


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 𝐴 → ( 𝐹 “ { 𝐵 } ) = { 𝑥𝐴 ∣ ( 𝐹𝑥 ) = 𝐵 } )