Theorem reldm0 5168

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 5075	. . 3 |- Rel (/)
2		eqrel 5040	. . 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 3763	. . 3 |- ( dom A = (/) <-> A. x -. x e. dom A )
5		alnex 1589	. . . . . 6 |- ( A. y -. <. x , y >. e. A <-> -. E. y <. x , y >. e. A )
6		vex 3081	. . . . . . 7 |- x e. _V
7	6	eldm2 5149	. . . . . 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 3752	. . . . . . 7 |- -. <. x , y >. e. (/)
10	9	nbn 347	. . . . . 6 |- ( -. <. x , y >. e. A <-> ( <. x , y >. e. A <-> <. x , y >. e. (/) ) )
11	10	albii 1611	. . . . 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 1611	. . 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 1368   = wceq 1370   E.wex 1587   e. wcel 1758   (/)c0 3748   <.cop 3994   dom cdm 4951   Rel wrel 4956

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432  ax-sep 4524  ax-nul 4532  ax-pr 4642

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2650  df-rab 2808  df-v 3080  df-dif 3442  df-un 3444  df-in 3446  df-ss 3453  df-nul 3749  df-if 3903  df-sn 3989  df-pr 3991  df-op 3995  df-br 4404  df-opab 4462  df-xp 4957  df-rel 4958  df-dm 4961

This theorem is referenced by:  relrn0  5208  fnresdisj  5632  fn0  5641  fresaunres2  5694  fsnunfv  6030  frxp  6795  domss2  7583  setsres  14323  pmtrsn  16147  gsumval3OLD  16506  gsumval3  16509  00lsp  17188  metn0  20070  eupath  23774  dfrdg2  27773  mbfresfi  28606  mapfzcons1  29221  coeq0  29258  diophrw  29265  eldioph2lem1  29266  eldioph2lem2  29267  wlkn0  30447  usgravd00  30706