Theorem eq0rdv 4372

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4  ∀wal 1568   = wceq 1570   ∈ wcel 2146  ∅c0 4286

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-dif 3909  df-nul 4287

This theorem is used by:  map0b  8887  disjen  9129  mapdom1  9137  pwxpndom2  10665  fzdisj  13596  smu01lem  16565  prmreclem5  17002  vdwap0  17058  natfval  18028  fucbas  18042  fuchom  18043  coafval  18143  efgval  19831  lsppratlem6  21326  lbsextlem4  21335  0ringprmidl  21527  psrvscafval  22148  cfinufil  24136  ufinffr  24137  fin1aufil  24140  bldisj  24606  reconnlem1  25035  pcofval  25220  bcthlem5  25538  volfiniun  25757  fta1g  26378  fta1  26520  rpvmasum  27741  0ringmon1p  33911  0ringirng  34143  unblimceq0  37153  bj-ab0  37600  bj-projval  37689  finxpnom  38104  ipo0  45216  ifr0  45217  limclner  46423  iineq0  49655