Theorem eq0rdv 4356

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

Syntax hints:  ¬ wn 3   → wi 4  ∀wal 1539   = wceq 1541   ∈ wcel 2113  ∅c0 4282

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-dif 3901  df-nul 4283

This theorem is referenced by:  map0b  8817  disjen  9058  mapdom1  9066  pwxpndom2  10567  fzdisj  13458  smu01lem  16403  prmreclem5  16839  vdwap0  16895  natfval  17864  fucbas  17878  fuchom  17879  coafval  17979  efgval  19637  lsppratlem6  21098  lbsextlem4  21107  psrvscafval  21895  cfinufil  23863  ufinffr  23864  fin1aufil  23867  bldisj  24333  reconnlem1  24762  pcofval  24957  bcthlem5  25275  volfiniun  25495  fta1g  26122  fta1  26263  rpvmasum  27484  0ringprmidl  33458  0ringmon1p  33566  0ringirng  33774  unblimceq0  36623  bj-ab0  37025  bj-projval  37113  finxpnom  37518  ipo0  44605  ifr0  44606  limclner  45811  iineq0  48981