Theorem eq0rdv 4372

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

Syntax hints:  ¬ wn 3   → wi 4  ∀wal 1568   = wceq 1570   ∈ wcel 2143  ∅c0 4286

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-dif 3908  df-nul 4287

This theorem is referenced by:  map0b  8877  disjen  9118  mapdom1  9126  pwxpndom2  10645  fzdisj  13575  smu01lem  16538  prmreclem5  16975  vdwap0  17031  natfval  18001  fucbas  18015  fuchom  18016  coafval  18116  efgval  19782  lsppratlem6  21276  lbsextlem4  21285  0ringprmidl  21477  psrvscafval  22098  cfinufil  24085  ufinffr  24086  fin1aufil  24089  bldisj  24555  reconnlem1  24984  pcofval  25169  bcthlem5  25487  volfiniun  25706  fta1g  26327  fta1  26469  rpvmasum  27690  0ringmon1p  33847  0ringirng  34079  unblimceq0  37096  bj-ab0  37543  bj-projval  37632  finxpnom  38047  ipo0  45158  ifr0  45159  limclner  46365  iineq0  49598