Theorem eq0rdv 4361

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 4304	. 2 ⊢ (𝐴 = ∅ ↔ ∀𝑥 ¬ 𝑥 ∈ 𝐴)
4	2, 3	sylibr 234	1 ⊢ (𝜑 → 𝐴 = ∅)

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

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 3906  df-nul 4288

This theorem is referenced by:  map0b  8833  disjen  9074  mapdom1  9082  pwxpndom2  10588  fzdisj  13479  smu01lem  16424  prmreclem5  16860  vdwap0  16916  natfval  17885  fucbas  17899  fuchom  17900  coafval  18000  efgval  19658  lsppratlem6  21119  lbsextlem4  21128  psrvscafval  21916  cfinufil  23884  ufinffr  23885  fin1aufil  23888  bldisj  24354  reconnlem1  24783  pcofval  24978  bcthlem5  25296  volfiniun  25516  fta1g  26143  fta1  26284  rpvmasum  27505  0ringprmidl  33542  0ringmon1p  33650  0ringirng  33867  unblimceq0  36729  bj-ab0  37156  bj-projval  37244  finxpnom  37656  ipo0  44804  ifr0  44805  limclner  46009  iineq0  49179