Theorem eq0rdv 4335

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

Syntax hints:  ¬ wn 3   → wi 4  ∀wal 1545   = wceq 1547   ∈ wcel 2119  ∅c0 4261

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-dif 3886  df-nul 4262

This theorem is referenced by:  map0b  8821  disjen  9062  mapdom1  9070  pwxpndom2  10579  fzdisj  13496  smu01lem  16445  prmreclem5  16882  vdwap0  16938  natfval  17907  fucbas  17921  fuchom  17922  coafval  18022  efgval  19683  lsppratlem6  21145  lbsextlem4  21154  psrvscafval  21923  cfinufil  23911  ufinffr  23912  fin1aufil  23915  bldisj  24381  reconnlem1  24810  pcofval  24995  bcthlem5  25313  volfiniun  25532  fta1g  26153  fta1  26292  rpvmasum  27507  0ringprmidl  33532  0ringmon1p  33640  0ringirng  33873  unblimceq0  36813  bj-ab0  37261  bj-projval  37349  finxpnom  37763  ipo0  44892  ifr0  44893  limclner  46094  iineq0  49310