Theorem eq0rdv 4407

Description: Deduction for equality to the empty set. (Contributed by NM, 11-Jul-2014.) Avoid ax-8 2110, df-clel 2816. (Revised by GG, 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 1927	. 2 ⊢ (𝜑 → ∀𝑥 ¬ 𝑥 ∈ 𝐴)
3		dfnul4 4335	. . . 4 ⊢ ∅ = {𝑦 ∣ ⊥}
4	3	eqeq2i 2750	. . 3 ⊢ (𝐴 = ∅ ↔ 𝐴 = {𝑦 ∣ ⊥})
5		dfcleq 2730	. . 3 ⊢ (𝐴 = {𝑦 ∣ ⊥} ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ {𝑦 ∣ ⊥}))
6		df-clab 2715	. . . . . . 7 ⊢ (𝑥 ∈ {𝑦 ∣ ⊥} ↔ [𝑥 / 𝑦]⊥)
7		sbv 2088	. . . . . . 7 ⊢ ([𝑥 / 𝑦]⊥ ↔ ⊥)
8	6, 7	bitri 275	. . . . . 6 ⊢ (𝑥 ∈ {𝑦 ∣ ⊥} ↔ ⊥)
9	8	bibi2i 337	. . . . 5 ⊢ ((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ {𝑦 ∣ ⊥}) ↔ (𝑥 ∈ 𝐴 ↔ ⊥))
10	9	albii 1819	. . . 4 ⊢ (∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ {𝑦 ∣ ⊥}) ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ ⊥))
11		nbfal 1555	. . . . . 6 ⊢ (¬ 𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐴 ↔ ⊥))
12	11	bicomi 224	. . . . 5 ⊢ ((𝑥 ∈ 𝐴 ↔ ⊥) ↔ ¬ 𝑥 ∈ 𝐴)
13	12	albii 1819	. . . 4 ⊢ (∀𝑥(𝑥 ∈ 𝐴 ↔ ⊥) ↔ ∀𝑥 ¬ 𝑥 ∈ 𝐴)
14	10, 13	bitri 275	. . 3 ⊢ (∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ {𝑦 ∣ ⊥}) ↔ ∀𝑥 ¬ 𝑥 ∈ 𝐴)
15	4, 5, 14	3bitrri 298	. 2 ⊢ (∀𝑥 ¬ 𝑥 ∈ 𝐴 ↔ 𝐴 = ∅)
16	2, 15	sylib 218	1 ⊢ (𝜑 → 𝐴 = ∅)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206  ∀wal 1538   = wceq 1540  ⊥wfal 1552  [wsb 2064   ∈ wcel 2108  {cab 2714  ∅c0 4333

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-dif 3954  df-nul 4334

This theorem is referenced by:  map0b  8923  disjen  9174  mapdom1  9182  pwxpndom2  10705  fzdisj  13591  smu01lem  16522  prmreclem5  16958  vdwap0  17014  natfval  17994  fucbas  18008  fuchom  18009  coafval  18109  efgval  19735  lsppratlem6  21154  lbsextlem4  21163  psrvscafval  21968  cfinufil  23936  ufinffr  23937  fin1aufil  23940  bldisj  24408  reconnlem1  24848  pcofval  25043  bcthlem5  25362  volfiniun  25582  fta1g  26209  fta1  26350  rpvmasum  27570  0ringprmidl  33477  0ringmon1p  33583  0ringirng  33739  unblimceq0  36508  bj-ab0  36909  bj-projval  36997  finxpnom  37402  ipo0  44468  ifr0  44469  limclner  45666