Theorem eq0rdv 4370

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

Syntax hints:  ¬ wn 3   → wi 4  ∀wal 1565   = wceq 1567   ∈ wcel 2149  ∅c0 4294

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-dif 3916  df-nul 4295

This theorem is referenced by:  map0b  8877  disjen  9118  mapdom1  9126  pwxpndom2  10646  fzdisj  13575  smu01lem  16539  prmreclem5  16976  vdwap0  17032  natfval  18002  fucbas  18016  fuchom  18017  coafval  18117  efgval  19783  lsppratlem6  21250  lbsextlem4  21259  0ringprmidl  21442  psrvscafval  22063  cfinufil  24050  ufinffr  24051  fin1aufil  24054  bldisj  24520  reconnlem1  24949  pcofval  25134  bcthlem5  25452  volfiniun  25671  fta1g  26292  fta1  26434  rpvmasum  27652  0ringmon1p  33788  0ringirng  34020  unblimceq0  36981  bj-ab0  37428  bj-projval  37516  finxpnom  37930  ipo0  45045  ifr0  45046  limclner  46252  iineq0  49478