Theorem eq0rdv 3931

Description: Deduction rule for equality to the empty set. (Contributed by NM, 11-Jul-2014.)

Hypothesis

Ref	Expression
eq0rdv.1	⊢ (𝜑 → ¬ 𝑥 ∈ 𝐴)

Assertion

Ref	Expression
eq0rdv	⊢ (𝜑 → 𝐴 = ∅)

Distinct variable groups:   𝑥,𝐴   𝜑,𝑥

Proof of Theorem eq0rdv

Step	Hyp	Ref	Expression
1		eq0rdv.1	. . . 4 ⊢ (𝜑 → ¬ 𝑥 ∈ 𝐴)
2	1	pm2.21d 117	. . 3 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → 𝑥 ∈ ∅))
3	2	ssrdv 3574	. 2 ⊢ (𝜑 → 𝐴 ⊆ ∅)
4		ss0 3926	. 2 ⊢ (𝐴 ⊆ ∅ → 𝐴 = ∅)
5	3, 4	syl 17	1 ⊢ (𝜑 → 𝐴 = ∅)

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1475   ∈ wcel 1977   ⊆ wss 3540  ∅c0 3874

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-dif 3543  df-in 3547  df-ss 3554  df-nul 3875

This theorem is referenced by:  map0b  7782  disjen  8002  mapdom1  8010  pwxpndom2  9366  fzdisj  12239  smu01lem  15045  prmreclem5  15462  vdwap0  15518  natfval  16429  fucbas  16443  fuchom  16444  coafval  16537  efgval  17953  lsppratlem6  18973  lbsextlem4  18982  psrvscafval  19211  cfinufil  21542  ufinffr  21543  fin1aufil  21546  bldisj  22013  reconnlem1  22437  pcofval  22618  bcthlem5  22933  volfiniun  23122  fta1g  23731  fta1  23867  rpvmasum  25015  bj-projval  32177  finxpnom  32414  ipo0  37674  ifr0  37675  limclner  38718