Theorem eq0rdv 4347

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

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

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 2708

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 2715  df-cleq 2728  df-dif 3892  df-nul 4274

This theorem is referenced by:  map0b  8831  disjen  9072  mapdom1  9080  pwxpndom2  10588  fzdisj  13505  smu01lem  16454  prmreclem5  16891  vdwap0  16947  natfval  17916  fucbas  17930  fuchom  17931  coafval  18031  efgval  19692  lsppratlem6  21150  lbsextlem4  21159  psrvscafval  21927  cfinufil  23893  ufinffr  23894  fin1aufil  23897  bldisj  24363  reconnlem1  24792  pcofval  24977  bcthlem5  25295  volfiniun  25514  fta1g  26135  fta1  26274  rpvmasum  27489  0ringprmidl  33509  0ringmon1p  33617  0ringirng  33833  unblimceq0  36767  bj-ab0  37215  bj-projval  37303  finxpnom  37717  ipo0  44875  ifr0  44876  limclner  46079  iineq0  49295