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

Theorem eq0rdv 3774
Description: Deduction rule for equality to the empty set. (Contributed by NM, 11-Jul-2014.)
Hypothesis
Ref Expression
eq0rdv.1  |-  ( ph  ->  -.  x  e.  A
)
Assertion
Ref Expression
eq0rdv  |-  ( ph  ->  A  =  (/) )
Distinct variable groups:    x, A    ph, x

Proof of Theorem eq0rdv
StepHypRef Expression
1 eq0rdv.1 . . . 4  |-  ( ph  ->  -.  x  e.  A
)
21pm2.21d 106 . . 3  |-  ( ph  ->  ( x  e.  A  ->  x  e.  (/) ) )
32ssrdv 3448 . 2  |-  ( ph  ->  A  C_  (/) )
4 ss0 3770 . 2  |-  ( A 
C_  (/)  ->  A  =  (/) )
53, 4syl 17 1  |-  ( ph  ->  A  =  (/) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1405    e. wcel 1842    C_ wss 3414   (/)c0 3738
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380
This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-v 3061  df-dif 3417  df-in 3421  df-ss 3428  df-nul 3739
This theorem is referenced by:  map0b  7495  disjen  7712  mapdom1  7720  pwxpndom2  9073  fzdisj  11766  smu01lem  14344  prmreclem5  14647  vdwap0  14703  natfval  15559  fucbas  15573  fuchom  15574  coafval  15667  efgval  17059  lsppratlem6  18118  lbsextlem4  18127  psrvscafval  18363  cfinufil  20721  ufinffr  20722  fin1aufil  20725  bldisj  21193  reconnlem1  21623  pcofval  21802  bcthlem5  22059  volfiniun  22249  fta1g  22860  fta1  22996  rpvmasum  24092  bj-projval  31119  ipo0  36206  ifr0  36207  limclner  37025
  Copyright terms: Public domain W3C validator