Theorem reldm0 5069

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 4975	. . 3 |- Rel (/)
2		eqrel 4941	. . 3 |- ( ( Rel A /\ Rel (/) ) -> ( A = (/) <-> A. x A. y ( <. x , y >. e. A <-> <. x , y >. e. (/) ) ) )
3	1, 2	mpan2 676	. 2 |- ( Rel A -> ( A = (/) <-> A. x A. y ( <. x , y >. e. A <-> <. x , y >. e. (/) ) ) )
4		eq0 3778	. . 3 |- ( dom A = (/) <-> A. x -. x e. dom A )
5		alnex 1662	. . . . . 6 |- ( A. y -. <. x , y >. e. A <-> -. E. y <. x , y >. e. A )
6		vex 3085	. . . . . . 7 |- x e. _V
7	6	eldm2 5050	. . . . . 6 |- ( x e. dom A <-> E. y <. x , y >. e. A )
8	5, 7	xchbinxr 313	. . . . 5 |- ( A. y -. <. x , y >. e. A <-> -. x e. dom A )
9		noel 3766	. . . . . . 7 |- -. <. x , y >. e. (/)
10	9	nbn 349	. . . . . 6 |- ( -. <. x , y >. e. A <-> ( <. x , y >. e. A <-> <. x , y >. e. (/) ) )
11	10	albii 1688	. . . . 5 |- ( A. y -. <. x , y >. e. A <-> A. y ( <. x , y >. e. A <-> <. x , y >. e. (/) ) )
12	8, 11	bitr3i 255	. . . 4 |- ( -. x e. dom A <-> A. y ( <. x , y >. e. A <-> <. x , y >. e. (/) ) )
13	12	albii 1688	. . 3 |- ( A. x -. x e. dom A <-> A. x A. y ( <. x , y >. e. A <-> <. x , y >. e. (/) ) )
14	4, 13	bitr2i 254	. 2 |- ( A. x A. y ( <. x , y >. e. A <-> <. x , y >. e. (/) ) <-> dom A = (/) )
15	3, 14	syl6bb 265	1 |- ( Rel A -> ( A = (/) <-> dom A = (/) ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 188   A.wal 1436   = wceq 1438   E.wex 1660   e. wcel 1869   (/)c0 3762   <.cop 4003   dom cdm 4851   Rel wrel 4856

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-5 1749  ax-6 1795  ax-7 1840  ax-9 1873  ax-10 1888  ax-11 1893  ax-12 1906  ax-13 2054  ax-ext 2401  ax-sep 4544  ax-nul 4553  ax-pr 4658

This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 985  df-tru 1441  df-ex 1661  df-nf 1665  df-sb 1788  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2573  df-ne 2621  df-rab 2785  df-v 3084  df-dif 3440  df-un 3442  df-in 3444  df-ss 3451  df-nul 3763  df-if 3911  df-sn 3998  df-pr 4000  df-op 4004  df-br 4422  df-opab 4481  df-xp 4857  df-rel 4858  df-dm 4861

This theorem is referenced by:  relrn0  5109  coeq0  5361  fnresdisj  5702  fn0  5711  fresaunres2  5770  fsnunfv  6117  frxp  6915  domss2  7735  swrd0  12786  setsres  15144  pmtrsn  17153  gsumval3  17534  00lsp  18197  metn0  21367  wlkn0  25247  usgravd00  25639  eupath  25701  dfrdg2  30443  mbfresfi  31945  mapfzcons1  35522  diophrw  35564  eldioph2lem1  35565  eldioph2lem2  35566  sge0cl  38055  funopsn  38761