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

Theorem eq0rdv 3783
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 3473 . 2  |-  ( ph  ->  A  C_  (/) )
4 ss0 3779 . 2  |-  ( A 
C_  (/)  ->  A  =  (/) )
53, 4syl 16 1  |-  ( ph  ->  A  =  (/) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1370    e. wcel 1758    C_ wss 3439   (/)c0 3748
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-v 3080  df-dif 3442  df-in 3446  df-ss 3453  df-nul 3749
This theorem is referenced by:  map0b  7364  disjen  7581  mapdom1  7589  pwxpndom2  8946  fzdisj  11596  smu01lem  13802  prmreclem5  14102  vdwap0  14158  natfval  14978  fucbas  14992  fuchom  14993  coafval  15054  efgval  16338  lsppratlem6  17359  lbsextlem4  17368  psrvscafval  17587  cfinufil  19636  ufinffr  19637  fin1aufil  19640  bldisj  20108  reconnlem1  20538  pcofval  20717  bcthlem5  20974  volfiniun  21164  fta1g  21775  fta1  21910  rpvmasum  22911  ipo0  29873  ifr0  29874  bj-projval  32841
  Copyright terms: Public domain W3C validator