Theorem eq0rdv 4365

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

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

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 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-dif 3902  df-nul 4280

This theorem is used by:  map0b  8904  disjen  9146  mapdom1  9154  pwxpndom2  10743  fzdisj  13678  smu01lem  16648  prmreclem5  17091  vdwap0  17147  natfval  18117  fucbas  18131  fuchom  18132  coafval  18232  efgval  19924  lsppratlem6  21423  lbsextlem4  21432  0ringprmidl  21626  psrvscafval  22249  cfinufil  24240  ufinffr  24241  fin1aufil  24244  bldisj  24710  reconnlem1  25139  pcofval  25324  bcthlem5  25642  volfiniun  25861  fta1g  26481  fta1  26622  rpvmasum  27846  0ringmon1p  34082  0ringirng  34314  unblimceq0  37353  bj-ab0  37800  bj-projval  37889  finxpnom  38304  ipo0  45417  ifr0  45418  limclner  46630  iineq0  49899