This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ F Fn A → F -1 B = x ∈ A | F ⁡ x = B

Proof

Step Hyp Ref Expression
1 fncnvima2 ⊢ F Fn A → F -1 B = x ∈ A | F ⁡ x ∈ B
2 fvex ⊢ F ⁡ x ∈ V
3 2 elsn ⊢ F ⁡ x ∈ B ↔ F ⁡ x = B
4 3 rabbii ⊢ x ∈ A | F ⁡ x ∈ B = x ∈ A | F ⁡ x = B
5 1 4 eqtrdi ⊢ F Fn A → F -1 B = x ∈ A | F ⁡ x = B