Theorem eq0rdv 4368

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4  ∀wal 1568   = wceq 1570   ∈ wcel 2147  ∅c0 4281

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-dif 4050  df-nul 4282

This theorem is used by:  map0b  8949  disjen  9191  mapdom1  9199  pwxpndom2  10789  fzdisj  13725  smu01lem  16699  prmreclem5  17142  vdwap0  17198  natfval  18174  fucbas  18188  fuchom  18189  coafval  18289  efgval  19982  lsppratlem6  21481  lbsextlem4  21490  0ringprmidl  21684  psrvscafval  22311  cfinufil  24302  ufinffr  24303  fin1aufil  24306  bldisj  24772  reconnlem1  25201  pcofval  25386  bcthlem5  25704  volfiniun  25923  fta1g  26543  fta1  26684  rpvmasum  27910  0ringmon1p  34192  0ringirng  34432  unblimceq0  37588  bj-ab0  38035  bj-projval  38124  finxpnom  38592  ipo0  45692  ifr0  45693  limclner  46934  iineq0  50262