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

Theorem eq0rdv 3502
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 98 . . 3  |-  ( ph  ->  ( x  e.  A  ->  x  e.  (/) ) )
32ssrdv 3198 . 2  |-  ( ph  ->  A  C_  (/) )
4 ss0 3498 . 2  |-  ( A 
C_  (/)  ->  A  =  (/) )
53, 4syl 15 1  |-  ( ph  ->  A  =  (/) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1632    e. wcel 1696    C_ wss 3165   (/)c0 3468
This theorem is referenced by:  map0b  6822  disjen  7034  mapdom1  7042  pwxpndom2  8303  fzdisj  10833  smu01lem  12692  prmreclem5  12983  vdwap0  13039  natfval  13836  fucbas  13850  fuchom  13851  coafval  13912  efgval  15042  lsppratlem6  15921  lbsextlem4  15930  psrvscafval  16151  cfinufil  17639  ufinffr  17640  fin1aufil  17643  bldisj  17971  reconnlem1  18347  pcofval  18524  bcthlem5  18766  volfiniun  18920  fta1g  19569  fta1  19704  rpvmasum  20691  ipo0  27755  ifr0  27756
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-v 2803  df-dif 3168  df-in 3172  df-ss 3179  df-nul 3469
  Copyright terms: Public domain W3C validator