Theorem eq0rdv 4404

Description: Deduction for equality to the empty set. (Contributed by NM, 11-Jul-2014.) Avoid ax-8 2108, df-clel 2810. (Revised by Gino Giotto, 6-Sep-2024.)

Hypothesis

Ref	Expression
eq0rdv.1	⊢ (𝜑 → ¬ 𝑥 ∈ 𝐴)

Assertion

Ref	Expression
eq0rdv	⊢ (𝜑 → 𝐴 = ∅)

Distinct variable groups:   𝑥,𝐴   𝜑,𝑥

Proof of Theorem eq0rdv

Dummy variable 𝑦 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		eq0rdv.1	. . 3 ⊢ (𝜑 → ¬ 𝑥 ∈ 𝐴)
2	1	alrimiv 1930	. 2 ⊢ (𝜑 → ∀𝑥 ¬ 𝑥 ∈ 𝐴)
3		dfnul4 4324	. . . 4 ⊢ ∅ = {𝑦 ∣ ⊥}
4	3	eqeq2i 2745	. . 3 ⊢ (𝐴 = ∅ ↔ 𝐴 = {𝑦 ∣ ⊥})
5		dfcleq 2725	. . 3 ⊢ (𝐴 = {𝑦 ∣ ⊥} ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ {𝑦 ∣ ⊥}))
6		df-clab 2710	. . . . . . 7 ⊢ (𝑥 ∈ {𝑦 ∣ ⊥} ↔ [𝑥 / 𝑦]⊥)
7		sbv 2091	. . . . . . 7 ⊢ ([𝑥 / 𝑦]⊥ ↔ ⊥)
8	6, 7	bitri 274	. . . . . 6 ⊢ (𝑥 ∈ {𝑦 ∣ ⊥} ↔ ⊥)
9	8	bibi2i 337	. . . . 5 ⊢ ((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ {𝑦 ∣ ⊥}) ↔ (𝑥 ∈ 𝐴 ↔ ⊥))
10	9	albii 1821	. . . 4 ⊢ (∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ {𝑦 ∣ ⊥}) ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ ⊥))
11		nbfal 1556	. . . . . 6 ⊢ (¬ 𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐴 ↔ ⊥))
12	11	bicomi 223	. . . . 5 ⊢ ((𝑥 ∈ 𝐴 ↔ ⊥) ↔ ¬ 𝑥 ∈ 𝐴)
13	12	albii 1821	. . . 4 ⊢ (∀𝑥(𝑥 ∈ 𝐴 ↔ ⊥) ↔ ∀𝑥 ¬ 𝑥 ∈ 𝐴)
14	10, 13	bitri 274	. . 3 ⊢ (∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ {𝑦 ∣ ⊥}) ↔ ∀𝑥 ¬ 𝑥 ∈ 𝐴)
15	4, 5, 14	3bitrri 297	. 2 ⊢ (∀𝑥 ¬ 𝑥 ∈ 𝐴 ↔ 𝐴 = ∅)
16	2, 15	sylib 217	1 ⊢ (𝜑 → 𝐴 = ∅)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205  ∀wal 1539   = wceq 1541  ⊥wfal 1553  [wsb 2067   ∈ wcel 2106  {cab 2709  ∅c0 4322

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-dif 3951  df-nul 4323

This theorem is referenced by:  map0b  8879  disjen  9136  mapdom1  9144  pwxpndom2  10662  fzdisj  13532  smu01lem  16430  prmreclem5  16857  vdwap0  16913  natfval  17901  fucbas  17916  fuchom  17917  fuchomOLD  17918  coafval  18018  efgval  19626  lsppratlem6  20910  lbsextlem4  20919  psrvscafval  21728  cfinufil  23652  ufinffr  23653  fin1aufil  23656  bldisj  24124  reconnlem1  24562  pcofval  24750  bcthlem5  25069  volfiniun  25288  fta1g  25909  fta1  26045  rpvmasum  27253  0ringprmidl  32830  0ringmon1p  32898  0ringirng  33030  unblimceq0  35686  bj-ab0  36091  bj-projval  36180  finxpnom  36585  ipo0  43510  ifr0  43511  limclner  44666