Metamath Proof Explorer

Theorem elmptima

Description: The image of a function in maps-to notation. (Contributed by Glauco Siliprandi, 2-Jan-2022)

Ref Expression
Assertion elmptima ⊢ C ∈ V → C ∈ x ∈ A ⟼ B D ↔ ∃ x ∈ A ∩ D C = B

Proof

Step Hyp Ref Expression
1 mptima ⊢ x ∈ A ⟼ B D = ran ⁡ x ∈ A ∩ D ⟼ B
2 1 a1i ⊢ C ∈ V → x ∈ A ⟼ B D = ran ⁡ x ∈ A ∩ D ⟼ B
3 2 eleq2d ⊢ C ∈ V → C ∈ x ∈ A ⟼ B D ↔ C ∈ ran ⁡ x ∈ A ∩ D ⟼ B
4 eqid ⊢ x ∈ A ∩ D ⟼ B = x ∈ A ∩ D ⟼ B
5 4 elrnmpt ⊢ C ∈ V → C ∈ ran ⁡ x ∈ A ∩ D ⟼ B ↔ ∃ x ∈ A ∩ D C = B
6 3 5 bitrd ⊢ C ∈ V → C ∈ x ∈ A ⟼ B D ↔ ∃ x ∈ A ∩ D C = B