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 = (/) ) )