MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  eq0rdv Unicode version

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
StepHypRef Expression
1 eq0rdv.1 . . . 4
21pm2.21d 106 . . 3
32ssrdv 3509 . 2
4 ss0 3816 . 2
53, 4syl 16 1
Colors of variables: wff setvar class
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
  Copyright terms: Public domain W3C validator