Theorem eq0rdv 4365

Description: Deduction for equality to the empty set. (Contributed by NM, 11-Jul-2014.) Avoid ax-8 2147, df-clel 2835. (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 2732

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 2739  df-cleq 2752  df-dif 3902  df-nul 4280

This theorem is used by:  map0b  8890  disjen  9132  mapdom1  9140  pwxpndom2  10674  fzdisj  13606  smu01lem  16575  prmreclem5  17012  vdwap0  17068  natfval  18038  fucbas  18052  fuchom  18053  coafval  18153  efgval  19844  lsppratlem6  21339  lbsextlem4  21348  0ringprmidl  21540  psrvscafval  22163  cfinufil  24154  ufinffr  24155  fin1aufil  24158  bldisj  24624  reconnlem1  25053  pcofval  25238  bcthlem5  25556  volfiniun  25775  fta1g  26395  fta1  26538  rpvmasum  27762  0ringmon1p  33967  0ringirng  34199  unblimceq0  37204  bj-ab0  37651  bj-projval  37740  finxpnom  38155  ipo0  45272  ifr0  45273  limclner  46479  iineq0  49748