Theorem eq0rdv 4312

Description: Deduction 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 121	. . 3 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → 𝑥 ∈ ∅))
3	2	ssrdv 3921	. 2 ⊢ (𝜑 → 𝐴 ⊆ ∅)
4		ss0 4306	. 2 ⊢ (𝐴 ⊆ ∅ → 𝐴 = ∅)
5	3, 4	syl 17	1 ⊢ (𝜑 → 𝐴 = ∅)

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1538   ∈ wcel 2111   ⊆ wss 3881  ∅c0 4243

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-dif 3884  df-in 3888  df-ss 3898  df-nul 4244

This theorem is referenced by:  map0b  8430  disjen  8658  mapdom1  8666  pwxpndom2  10076  fzdisj  12929  smu01lem  15824  prmreclem5  16246  vdwap0  16302  natfval  17208  fucbas  17222  fuchom  17223  coafval  17316  efgval  18835  lsppratlem6  19917  lbsextlem4  19926  psrvscafval  20628  cfinufil  22533  ufinffr  22534  fin1aufil  22537  bldisj  23005  reconnlem1  23431  pcofval  23615  bcthlem5  23932  volfiniun  24151  fta1g  24768  fta1  24904  rpvmasum  26110  0ringprmidl  31033  unblimceq0  33959  bj-projval  34432  finxpnom  34818  ipo0  41153  ifr0  41154  limclner  42293