Metamath Proof Explorer

Theorem fniniseg

Description: Membership in the preimage of a singleton, under a function. (Contributed by Mario Carneiro, 12-May-2014) (Proof shortened by Mario Carneiro , 28-Apr-2015)

Ref Expression
Assertion fniniseg ⊢ F Fn A → C ∈ F -1 B ↔ C ∈ A ∧ F ⁡ C = B

Proof

Step Hyp Ref Expression
1 elpreima ⊢ F Fn A → C ∈ F -1 B ↔ C ∈ A ∧ F ⁡ C ∈ B
2 fvex ⊢ F ⁡ C ∈ V
3 2 elsn ⊢ F ⁡ C ∈ B ↔ F ⁡ C = B
4 3 anbi2i ⊢ C ∈ A ∧ F ⁡ C ∈ B ↔ C ∈ A ∧ F ⁡ C = B
5 1 4 bitrdi ⊢ F Fn A → C ∈ F -1 B ↔ C ∈ A ∧ F ⁡ C = B