Theorem reldm0 5206

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

Assertion

Ref	Expression
reldm0	|- ( Rel A -> ( A = (/) <-> dom A = (/) ) )

Proof of Theorem reldm0

Dummy variables x y are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		rel0 5113	. . 3 |- Rel (/)
2		eqrel 5078	. . 3 |- ( ( Rel A /\ Rel (/) ) -> ( A = (/) <-> A. x A. y ( <. x , y >. e. A <-> <. x , y >. e. (/) ) ) )
3	1, 2	mpan2 671	. 2 |- ( Rel A -> ( A = (/) <-> A. x A. y ( <. x , y >. e. A <-> <. x , y >. e. (/) ) ) )
4		eq0 3782	. . 3 |- ( dom A = (/) <-> A. x -. x e. dom A )
5		alnex 1599	. . . . . 6 |- ( A. y -. <. x , y >. e. A <-> -. E. y <. x , y >. e. A )
6		vex 3096	. . . . . . 7 |- x e. _V
7	6	eldm2 5187	. . . . . 6 |- ( x e. dom A <-> E. y <. x , y >. e. A )
8	5, 7	xchbinxr 311	. . . . 5 |- ( A. y -. <. x , y >. e. A <-> -. x e. dom A )
9		noel 3771	. . . . . . 7 |- -. <. x , y >. e. (/)
10	9	nbn 347	. . . . . 6 |- ( -. <. x , y >. e. A <-> ( <. x , y >. e. A <-> <. x , y >. e. (/) ) )
11	10	albii 1625	. . . . 5 |- ( A. y -. <. x , y >. e. A <-> A. y ( <. x , y >. e. A <-> <. x , y >. e. (/) ) )
12	8, 11	bitr3i 251	. . . 4 |- ( -. x e. dom A <-> A. y ( <. x , y >. e. A <-> <. x , y >. e. (/) ) )
13	12	albii 1625	. . 3 |- ( A. x -. x e. dom A <-> A. x A. y ( <. x , y >. e. A <-> <. x , y >. e. (/) ) )
14	4, 13	bitr2i 250	. 2 |- ( A. x A. y ( <. x , y >. e. A <-> <. x , y >. e. (/) ) <-> dom A = (/) )
15	3, 14	syl6bb 261	1 |- ( Rel A -> ( A = (/) <-> dom A = (/) ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 184   A.wal 1379   = wceq 1381   E.wex 1597   e. wcel 1802   (/)c0 3767   <.cop 4016   dom cdm 4985   Rel wrel 4990

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-9 1806  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419  ax-sep 4554  ax-nul 4562  ax-pr 4672

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 974  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-clab 2427  df-cleq 2433  df-clel 2436  df-nfc 2591  df-ne 2638  df-rab 2800  df-v 3095  df-dif 3461  df-un 3463  df-in 3465  df-ss 3472  df-nul 3768  df-if 3923  df-sn 4011  df-pr 4013  df-op 4017  df-br 4434  df-opab 4492  df-xp 4991  df-rel 4992  df-dm 4995

This theorem is referenced by:  relrn0  5246  coeq0  5502  fnresdisj  5677  fn0  5686  fresaunres2  5743  fsnunfv  6092  frxp  6891  domss2  7674  setsres  14532  pmtrsn  16413  gsumval3OLD  16777  gsumval3  16780  00lsp  17495  metn0  20729  wlkn0  24392  usgravd00  24784  eupath  24846  dfrdg2  29196  mbfresfi  30029  mapfzcons1  30617  diophrw  30660  eldioph2lem1  30661  eldioph2lem2  30662