Metamath Proof Explorer

Theorem elimampt

Description: Membership in the image of a mapping. (Contributed by Thierry Arnoux, 3-Jan-2022)

Ref Expression
Hypotheses elimampt.f ⊢ F = x ∈ A ⟼ B
elimampt.c ⊢ φ → C ∈ W
elimampt.d ⊢ φ → D ⊆ A
Assertion elimampt ⊢ φ → C ∈ F D ↔ ∃ x ∈ D C = B

Proof

Step Hyp Ref Expression
1 elimampt.f ⊢ F = x ∈ A ⟼ B
2 elimampt.c ⊢ φ → C ∈ W
3 elimampt.d ⊢ φ → D ⊆ A
4 df-ima ⊢ F D = ran ⁡ F ↾ D
5 4 eleq2i ⊢ C ∈ F D ↔ C ∈ ran ⁡ F ↾ D
6 1 reseq1i ⊢ F ↾ D = x ∈ A ⟼ B ↾ D
7 resmpt ⊢ D ⊆ A → x ∈ A ⟼ B ↾ D = x ∈ D ⟼ B
8 6 7 eqtrid ⊢ D ⊆ A → F ↾ D = x ∈ D ⟼ B
9 8 rneqd ⊢ D ⊆ A → ran ⁡ F ↾ D = ran ⁡ x ∈ D ⟼ B
10 9 eleq2d ⊢ D ⊆ A → C ∈ ran ⁡ F ↾ D ↔ C ∈ ran ⁡ x ∈ D ⟼ B
11 3 10 syl ⊢ φ → C ∈ ran ⁡ F ↾ D ↔ C ∈ ran ⁡ x ∈ D ⟼ B
12 eqid ⊢ x ∈ D ⟼ B = x ∈ D ⟼ B
13 12 elrnmpt ⊢ C ∈ W → C ∈ ran ⁡ x ∈ D ⟼ B ↔ ∃ x ∈ D C = B
14 2 13 syl ⊢ φ → C ∈ ran ⁡ x ∈ D ⟼ B ↔ ∃ x ∈ D C = B
15 11 14 bitrd ⊢ φ → C ∈ ran ⁡ F ↾ D ↔ ∃ x ∈ D C = B
16 5 15 syl5bb ⊢ φ → C ∈ F D ↔ ∃ x ∈ D C = B