Theorem eq0rdv 4348

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

Syntax hints:  ¬ wn 3   → wi 4  ∀wal 1540   = wceq 1542   ∈ wcel 2114  ∅c0 4274

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 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-dif 3893  df-nul 4275

This theorem is referenced by:  map0b  8824  disjen  9065  mapdom1  9073  pwxpndom2  10579  fzdisj  13496  smu01lem  16445  prmreclem5  16882  vdwap0  16938  natfval  17907  fucbas  17921  fuchom  17922  coafval  18022  efgval  19683  lsppratlem6  21142  lbsextlem4  21151  psrvscafval  21937  cfinufil  23903  ufinffr  23904  fin1aufil  23907  bldisj  24373  reconnlem1  24802  pcofval  24987  bcthlem5  25305  volfiniun  25524  fta1g  26145  fta1  26285  rpvmasum  27503  0ringprmidl  33524  0ringmon1p  33632  0ringirng  33849  unblimceq0  36783  bj-ab0  37231  bj-projval  37319  finxpnom  37731  ipo0  44893  ifr0  44894  limclner  46097  iineq0  49307