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

Theorem eq0rdv 3489
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 3185 . 2  |-  ( ph  ->  A  C_  (/) )
4 ss0 3485 . 2  |-  ( A 
C_  (/)  ->  A  =  (/) )
53, 4syl 15 1  |-  ( ph  ->  A  =  (/) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1623    e. wcel 1684    C_ wss 3152   (/)c0 3455
This theorem is referenced by:  map0b  6806  disjen  7018  mapdom1  7026  pwxpndom2  8287  fzdisj  10817  smu01lem  12676  prmreclem5  12967  vdwap0  13023  natfval  13820  fucbas  13834  fuchom  13835  coafval  13896  efgval  15026  lsppratlem6  15905  lbsextlem4  15914  psrvscafval  16135  cfinufil  17623  ufinffr  17624  fin1aufil  17627  bldisj  17955  reconnlem1  18331  pcofval  18508  bcthlem5  18750  volfiniun  18904  fta1g  19553  fta1  19688  rpvmasum  20675  ipo0  27652  ifr0  27653
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-v 2790  df-dif 3155  df-in 3159  df-ss 3166  df-nul 3456
  Copyright terms: Public domain W3C validator