Theorem eq0rdv 4351

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

Syntax hints:  ¬ wn 3   → wi 4  ∀wal 1548   = wceq 1550   ∈ wcel 2132  ∅c0 4276

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1805  ax-4 1819  ax-5 1920  ax-6 1977  ax-7 2018  ax-9 2142  ax-ext 2724

This theorem depends on definitions:  df-bi 209  df-an 399  df-tru 1553  df-fal 1563  df-ex 1790  df-sb 2081  df-clab 2731  df-cleq 2744  df-dif 3898  df-nul 4277

This theorem is referenced by:  map0b  8850  disjen  9091  mapdom1  9099  pwxpndom2  10609  fzdisj  13542  smu01lem  16491  prmreclem5  16928  vdwap0  16984  natfval  17954  fucbas  17968  fuchom  17969  coafval  18069  efgval  19729  lsppratlem6  21191  lbsextlem4  21200  psrvscafval  21969  cfinufil  23957  ufinffr  23958  fin1aufil  23961  bldisj  24427  reconnlem1  24856  pcofval  25041  bcthlem5  25359  volfiniun  25578  fta1g  26199  fta1  26338  rpvmasum  27556  0ringprmidl  33581  0ringmon1p  33697  0ringirng  33930  unblimceq0  36883  bj-ab0  37331  bj-projval  37419  finxpnom  37833  ipo0  44962  ifr0  44963  limclner  46163  iineq0  49379