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 = (/) <-> A. x A. y ( <. x , y >. e. A <-> <. x , y >. e. (/) ) ) )
3 1 2 mpan2
 |-  ( Rel A -> ( A = (/) <-> A. x A. y ( <. x , y >. e. A <-> <. x , y >. e. (/) ) ) )
4 eq0
 |-  ( dom A = (/) <-> A. x -. x e. dom A )
5 alnex
 |-  ( A. y -. <. x , y >. e. A <-> -. E. y <. x , y >. e. A )
6 vex
 |-  x e. _V
7 6 eldm2
 |-  ( x e. dom A <-> E. y <. x , y >. e. A )
8 5 7 xchbinxr
 |-  ( A. y -. <. x , y >. e. A <-> -. x e. dom A )
9 noel
 |-  -. <. x , y >. e. (/)
10 9 nbn
 |-  ( -. <. x , y >. e. A <-> ( <. x , y >. e. A <-> <. x , y >. e. (/) ) )
11 10 albii
 |-  ( A. y -. <. x , y >. e. A <-> A. y ( <. x , y >. e. A <-> <. x , y >. e. (/) ) )
12 8 11 bitr3i
 |-  ( -. x e. dom A <-> A. y ( <. x , y >. e. A <-> <. x , y >. e. (/) ) )
13 12 albii
 |-  ( A. x -. x e. dom A <-> A. x A. y ( <. x , y >. e. A <-> <. x , y >. e. (/) ) )
14 4 13 bitr2i
 |-  ( A. x A. y ( <. x , y >. e. A <-> <. x , y >. e. (/) ) <-> dom A = (/) )
15 3 14 bitrdi
 |-  ( Rel A -> ( A = (/) <-> dom A = (/) ) )