Metamath Proof Explorer


Theorem rnmpt0f

Description: The range of a function in maps-to notation is empty if and only if its domain is empty. (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
Assertion rnmpt0f φ ran F = A =

Proof

Step Hyp Ref Expression
1 rnmpt0f.1 x φ
2 rnmpt0f.2 φ x A B V
3 rnmpt0f.3 F = x A B
4 2 ex φ x A B V
5 1 4 ralrimi φ x A B V
6 dmmptg x A B V dom x A B = A
7 5 6 syl φ dom x A B = A
8 7 eqcomd φ A = dom x A B
9 8 eqeq1d φ A = dom x A B =
10 dm0rn0 dom x A B = ran x A B =
11 10 a1i φ dom x A B = ran x A B =
12 3 rneqi ran F = ran x A B
13 12 a1i φ ran F = ran x A B
14 13 eqcomd φ ran x A B = ran F
15 14 eqeq1d φ ran x A B = ran F =
16 9 11 15 3bitrrd φ ran F = A =