Metamath Proof Explorer

Theorem elpreima

Description: Membership in the preimage of a class under a function. (Contributed by Jeff Madsen, 2-Sep-2009) (Proof shortened by Sky Winter, 22-Oct-2026)

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

Proof

Step Hyp Ref Expression
1 cnvimass ⊢ F -1 C ⊆ dom ⁡ F
2 1 sseli ⊢ B ∈ F -1 C → B ∈ dom ⁡ F
3 fndm ⊢ F Fn A → dom ⁡ F = A
4 3 eleq2d ⊢ F Fn A → B ∈ dom ⁡ F ↔ B ∈ A
5 2 4 imbitrid ⊢ F Fn A → B ∈ F -1 C → B ∈ A
6 5 pm4.71rd ⊢ F Fn A → B ∈ F -1 C ↔ B ∈ A ∧ B ∈ F -1 C
7 fvimacnv ⊢ Fun ⁡ F ∧ B ∈ dom ⁡ F → F ⁡ B ∈ C ↔ B ∈ F -1 C
8 7 funfni ⊢ F Fn A ∧ B ∈ A → F ⁡ B ∈ C ↔ B ∈ F -1 C
9 8 pm5.32da ⊢ F Fn A → B ∈ A ∧ F ⁡ B ∈ C ↔ B ∈ A ∧ B ∈ F -1 C
10 6 9 bitr4d ⊢ F Fn A → B ∈ F -1 C ↔ B ∈ A ∧ F ⁡ B ∈ C