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

Theorem eq0rdv 3781
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 110 . . 3  |-  ( ph  ->  ( x  e.  A  ->  x  e.  (/) ) )
32ssrdv 3450 . 2  |-  ( ph  ->  A  C_  (/) )
4 ss0 3777 . 2  |-  ( A 
C_  (/)  ->  A  =  (/) )
53, 4syl 17 1  |-  ( ph  ->  A  =  (/) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1455    e. wcel 1898    C_ wss 3416   (/)c0 3743
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442
This theorem depends on definitions:  df-bi 190  df-an 377  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-v 3059  df-dif 3419  df-in 3423  df-ss 3430  df-nul 3744
This theorem is referenced by:  map0b  7536  disjen  7755  mapdom1  7763  pwxpndom2  9116  fzdisj  11855  smu01lem  14508  prmreclem5  14913  vdwap0  14975  natfval  15900  fucbas  15914  fuchom  15915  coafval  16008  efgval  17416  lsppratlem6  18424  lbsextlem4  18433  psrvscafval  18663  cfinufil  20992  ufinffr  20993  fin1aufil  20996  bldisj  21462  reconnlem1  21893  pcofval  22090  bcthlem5  22345  volfiniun  22549  fta1g  23167  fta1  23310  rpvmasum  24413  bj-projval  31635  finxpnom  31838  ipo0  36846  ifr0  36847  limclner  37770
  Copyright terms: Public domain W3C validator