Theorem eq0rdv 4364

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4  ∀wal 1567   = wceq 1569   ∈ wcel 2144  ∅c0 4277

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-dif 4046  df-nul 4278

This theorem is used by:  map0b  8918  disjen  9160  mapdom1  9168  pwxpndom2  10757  fzdisj  13692  smu01lem  16664  prmreclem5  17107  vdwap0  17163  natfval  18133  fucbas  18147  fuchom  18148  coafval  18248  efgval  19940  lsppratlem6  21439  lbsextlem4  21448  0ringprmidl  21642  psrvscafval  22265  cfinufil  24256  ufinffr  24257  fin1aufil  24260  bldisj  24726  reconnlem1  25155  pcofval  25340  bcthlem5  25658  volfiniun  25877  fta1g  26497  fta1  26638  rpvmasum  27862  0ringmon1p  34139  0ringirng  34371  unblimceq0  37469  bj-ab0  37916  bj-projval  38005  finxpnom  38433  ipo0  45540  ifr0  45541  limclner  46769  iineq0  50039