Theorem eq0rdv 3820

Description: Deduction rule for equality to the empty set. (Contributed by NM, 11-Jul-2014.)

Hypothesis

Ref	Expression
eq0rdv.1

Assertion

Ref	Expression
eq0rdv

Distinct variable groups:   ,   ,

Proof of Theorem eq0rdv

Step	Hyp	Ref	Expression
1		eq0rdv.1	. . . 4
2	1	pm2.21d 106	. . 3
3	2	ssrdv 3509	. 2
4		ss0 3816	. 2
5	3, 4	syl 16	1

Syntax hints:  -.wn 3  ->wi 4  =wceq 1395  e.wcel 1818  C_wss 3475  c0 3784

This theorem is referenced by:  map0b  7477  disjen  7694  mapdom1  7702  pwxpndom2  9064  fzdisj  11741  smu01lem  14135  prmreclem5  14438  vdwap0  14494  natfval  15315  fucbas  15329  fuchom  15330  coafval  15391  efgval  16735  lsppratlem6  17798  lbsextlem4  17807  psrvscafval  18043  cfinufil  20429  ufinffr  20430  fin1aufil  20433  bldisj  20901  reconnlem1  21331  pcofval  21510  bcthlem5  21767  volfiniun  21957  fta1g  22568  fta1  22704  rpvmasum  23711  ipo0  31358  ifr0  31359  limclner  31657  bj-projval  34554

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-v 3111  df-dif 3478  df-in 3482  df-ss 3489  df-nul 3785