Theorem eq0rdv 4358

Description: Deduction for equality to the empty set. (Contributed by NM, 11-Jul-2014.) Avoid ax-8 2143, df-clel 2836. (Revised by GG, 6-Sep-2024.)

Hypothesis

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

Assertion

Ref	Expression
eq0rdv	⊢ (𝜑 → 𝐴 = ∅)

Distinct variable groups:   𝑥,𝐴   𝜑,𝑥

Proof of Theorem eq0rdv

Step	Hyp	Ref	Expression
1		eq0rdv.1	. . 3 ⊢ (𝜑 → ¬ 𝑥 ∈ 𝐴)
2	1	alrimiv 1946	. 2 ⊢ (𝜑 → ∀𝑥 ¬ 𝑥 ∈ 𝐴)
3		eq0 4300	. 2 ⊢ (𝐴 = ∅ ↔ ∀𝑥 ¬ 𝑥 ∈ 𝐴)
4	2, 3	sylibr 236	1 ⊢ (𝜑 → 𝐴 = ∅)

Syntax hints:  ¬ wn 3   → wi 4  ∀wal 1557   = wceq 1559   ∈ wcel 2141  ∅c0 4283

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1562  df-fal 1572  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-dif 3905  df-nul 4284

This theorem is referenced by:  map0b  8859  disjen  9100  mapdom1  9108  pwxpndom2  10617  fzdisj  13550  smu01lem  16510  prmreclem5  16947  vdwap0  17003  natfval  17973  fucbas  17987  fuchom  17988  coafval  18088  efgval  19748  lsppratlem6  21210  lbsextlem4  21219  psrvscafval  21988  cfinufil  23976  ufinffr  23977  fin1aufil  23980  bldisj  24446  reconnlem1  24875  pcofval  25060  bcthlem5  25378  volfiniun  25597  fta1g  26218  fta1  26360  rpvmasum  27578  0ringprmidl  33597  0ringmon1p  33714  0ringirng  33947  unblimceq0  36906  bj-ab0  37354  bj-projval  37442  finxpnom  37856  ipo0  44985  ifr0  44986  limclner  46186  iineq0  49402