Theorem eq0rdv 4359

Description: Deduction for equality to the empty set. (Contributed by NM, 11-Jul-2014.) Avoid ax-8 2115, df-clel 2811. (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 1928	. 2 ⊢ (𝜑 → ∀𝑥 ¬ 𝑥 ∈ 𝐴)
3		eq0 4302	. 2 ⊢ (𝐴 = ∅ ↔ ∀𝑥 ¬ 𝑥 ∈ 𝐴)
4	2, 3	sylibr 234	1 ⊢ (𝜑 → 𝐴 = ∅)

Syntax hints:  ¬ wn 3   → wi 4  ∀wal 1539   = wceq 1541   ∈ wcel 2113  ∅c0 4285

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-dif 3904  df-nul 4286

This theorem is referenced by:  map0b  8821  disjen  9062  mapdom1  9070  pwxpndom2  10576  fzdisj  13467  smu01lem  16412  prmreclem5  16848  vdwap0  16904  natfval  17873  fucbas  17887  fuchom  17888  coafval  17988  efgval  19646  lsppratlem6  21107  lbsextlem4  21116  psrvscafval  21904  cfinufil  23872  ufinffr  23873  fin1aufil  23876  bldisj  24342  reconnlem1  24771  pcofval  24966  bcthlem5  25284  volfiniun  25504  fta1g  26131  fta1  26272  rpvmasum  27493  0ringprmidl  33530  0ringmon1p  33638  0ringirng  33846  unblimceq0  36707  bj-ab0  37109  bj-projval  37197  finxpnom  37606  ipo0  44689  ifr0  44690  limclner  45895  iineq0  49065