Metamath Proof Explorer


Theorem reldm0

Description: A relation is empty iff its domain is empty. (Contributed by NM, 15-Sep-2004)

Ref Expression
Assertion reldm0 Rel A A = dom A =

Proof

Step Hyp Ref Expression
1 rel0 Rel
2 eqrel Rel A Rel A = x y x y A x y
3 1 2 mpan2 Rel A A = x y x y A x y
4 eq0 dom A = x ¬ x dom A
5 alnex y ¬ x y A ¬ y x y A
6 vex x V
7 6 eldm2 x dom A y x y A
8 5 7 xchbinxr y ¬ x y A ¬ x dom A
9 noel ¬ x y
10 9 nbn ¬ x y A x y A x y
11 10 albii y ¬ x y A y x y A x y
12 8 11 bitr3i ¬ x dom A y x y A x y
13 12 albii x ¬ x dom A x y x y A x y
14 4 13 bitr2i x y x y A x y dom A =
15 3 14 bitrdi Rel A A = dom A =