This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem rnmptn0

Description: The range of a function in maps-to notation is nonempty if the domain is nonempty. (Contributed by Glauco Siliprandi, 8-Apr-2021)

Ref Expression
Hypotheses rnmpt0f.1 ⊢ Ⅎ x φ
rnmpt0f.2 ⊢ φ ∧ x ∈ A → B ∈ V
rnmpt0f.3 ⊢ F = x ∈ A ⟼ B
rnmptn0.a ⊢ φ → A ≠ ∅
Assertion rnmptn0 ⊢ φ → ran ⁡ F ≠ ∅

Proof

Step Hyp Ref Expression
1 rnmpt0f.1 ⊢ Ⅎ x φ
2 rnmpt0f.2 ⊢ φ ∧ x ∈ A → B ∈ V
3 rnmpt0f.3 ⊢ F = x ∈ A ⟼ B
4 rnmptn0.a ⊢ φ → A ≠ ∅
5 4 neneqd ⊢ φ → ¬ A = ∅
6 1 2 3 rnmpt0f ⊢ φ → ran ⁡ F = ∅ ↔ A = ∅
7 5 6 mtbird ⊢ φ → ¬ ran ⁡ F = ∅
8 7 neqned ⊢ φ → ran ⁡ F ≠ ∅