Metamath Proof Explorer

Theorem elrnmpt2d

Description: Elementhood in the range of a function in maps-to notation, deduction form. (Contributed by Rohan Ridenour, 3-Aug-2023)

Ref Expression
Hypotheses elrnmpt2d.1 ⊢ F = x ∈ A ⟼ B
elrnmpt2d.2 ⊢ φ → C ∈ ran ⁡ F
Assertion elrnmpt2d ⊢ φ → ∃ x ∈ A C = B

Proof

Step Hyp Ref Expression
1 elrnmpt2d.1 ⊢ F = x ∈ A ⟼ B
2 elrnmpt2d.2 ⊢ φ → C ∈ ran ⁡ F
3 1 elrnmpt ⊢ C ∈ ran ⁡ F → C ∈ ran ⁡ F ↔ ∃ x ∈ A C = B
4 3 ibi ⊢ C ∈ ran ⁡ F → ∃ x ∈ A C = B
5 2 4 syl ⊢ φ → ∃ x ∈ A C = B