Theorem reldm0 5133

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 5039	. . 3 |- Rel (/)
2		eqrel 5005	. . 3 |- ( ( Rel A /\ Rel (/) ) -> ( A = (/) <-> A. x A. y ( <. x , y >. e. A <-> <. x , y >. e. (/) ) ) )
3	1, 2	mpan2 669	. 2 |- ( Rel A -> ( A = (/) <-> A. x A. y ( <. x , y >. e. A <-> <. x , y >. e. (/) ) ) )
4		eq0 3727	. . 3 |- ( dom A = (/) <-> A. x -. x e. dom A )
5		alnex 1622	. . . . . 6 |- ( A. y -. <. x , y >. e. A <-> -. E. y <. x , y >. e. A )
6		vex 3037	. . . . . . 7 |- x e. _V
7	6	eldm2 5114	. . . . . 6 |- ( x e. dom A <-> E. y <. x , y >. e. A )
8	5, 7	xchbinxr 309	. . . . 5 |- ( A. y -. <. x , y >. e. A <-> -. x e. dom A )
9		noel 3715	. . . . . . 7 |- -. <. x , y >. e. (/)
10	9	nbn 345	. . . . . 6 |- ( -. <. x , y >. e. A <-> ( <. x , y >. e. A <-> <. x , y >. e. (/) ) )
11	10	albii 1648	. . . . 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 1648	. . 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 1397   = wceq 1399   E.wex 1620   e. wcel 1826   (/)c0 3711   <.cop 3950   dom cdm 4913   Rel wrel 4918

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-9 1830  ax-10 1845  ax-11 1850  ax-12 1862  ax-13 2006  ax-ext 2360  ax-sep 4488  ax-nul 4496  ax-pr 4601

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1402  df-ex 1621  df-nf 1625  df-sb 1748  df-clab 2368  df-cleq 2374  df-clel 2377  df-nfc 2532  df-ne 2579  df-rab 2741  df-v 3036  df-dif 3392  df-un 3394  df-in 3396  df-ss 3403  df-nul 3712  df-if 3858  df-sn 3945  df-pr 3947  df-op 3951  df-br 4368  df-opab 4426  df-xp 4919  df-rel 4920  df-dm 4923

This theorem is referenced by:  relrn0  5173  coeq0  5424  fnresdisj  5599  fn0  5608  fresaunres2  5665  fsnunfv  6013  frxp  6809  domss2  7595  swrd0  12570  setsres  14664  pmtrsn  16661  gsumval3OLD  17025  gsumval3  17028  00lsp  17740  metn0  20948  wlkn0  24648  usgravd00  25040  eupath  25102  dfrdg2  29393  mbfresfi  30226  mapfzcons1  30815  diophrw  30857  eldioph2lem1  30858  eldioph2lem2  30859