Theorem eq0rdv 4124

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 119	. . 3 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → 𝑥 ∈ ∅))
3	2	ssrdv 3759	. 2 ⊢ (𝜑 → 𝐴 ⊆ ∅)
4		ss0 4119	. 2 ⊢ (𝐴 ⊆ ∅ → 𝐴 = ∅)
5	3, 4	syl 17	1 ⊢ (𝜑 → 𝐴 = ∅)

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1631   ∈ wcel 2145   ⊆ wss 3724  ∅c0 4064

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751

This theorem depends on definitions:  df-bi 197  df-an 383  df-or 829  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-v 3353  df-dif 3727  df-in 3731  df-ss 3738  df-nul 4065

This theorem is referenced by:  map0b  8050  disjen  8274  mapdom1  8282  pwxpndom2  9690  fzdisj  12576  smu01lem  15416  prmreclem5  15832  vdwap0  15888  natfval  16814  fucbas  16828  fuchom  16829  coafval  16922  efgval  18338  lsppratlem6  19368  lbsextlem4  19377  psrvscafval  19606  cfinufil  21953  ufinffr  21954  fin1aufil  21957  bldisj  22424  reconnlem1  22850  pcofval  23030  bcthlem5  23345  volfiniun  23536  fta1g  24148  fta1  24284  rpvmasum  25437  bj-projval  33316  finxpnom  33576  ipo0  39179  ifr0  39180  limclner  40402