Theorem eq0rdv 4387

Description: Deduction for equality to the empty set. (Contributed by NM, 11-Jul-2014.) Avoid ax-8 2109, df-clel 2808. (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 1926	. 2 ⊢ (𝜑 → ∀𝑥 ¬ 𝑥 ∈ 𝐴)
3		dfnul4 4315	. . . 4 ⊢ ∅ = {𝑦 ∣ ⊥}
4	3	eqeq2i 2747	. . 3 ⊢ (𝐴 = ∅ ↔ 𝐴 = {𝑦 ∣ ⊥})
5		dfcleq 2727	. . 3 ⊢ (𝐴 = {𝑦 ∣ ⊥} ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ {𝑦 ∣ ⊥}))
6		df-clab 2713	. . . . . . 7 ⊢ (𝑥 ∈ {𝑦 ∣ ⊥} ↔ [𝑥 / 𝑦]⊥)
7		sbv 2087	. . . . . . 7 ⊢ ([𝑥 / 𝑦]⊥ ↔ ⊥)
8	6, 7	bitri 275	. . . . . 6 ⊢ (𝑥 ∈ {𝑦 ∣ ⊥} ↔ ⊥)
9	8	bibi2i 337	. . . . 5 ⊢ ((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ {𝑦 ∣ ⊥}) ↔ (𝑥 ∈ 𝐴 ↔ ⊥))
10	9	albii 1818	. . . 4 ⊢ (∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ {𝑦 ∣ ⊥}) ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ ⊥))
11		nbfal 1554	. . . . . 6 ⊢ (¬ 𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐴 ↔ ⊥))
12	11	bicomi 224	. . . . 5 ⊢ ((𝑥 ∈ 𝐴 ↔ ⊥) ↔ ¬ 𝑥 ∈ 𝐴)
13	12	albii 1818	. . . 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 1537   = wceq 1539  ⊥wfal 1551  [wsb 2063   ∈ wcel 2107  {cab 2712  ∅c0 4313

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-9 2117  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1542  df-fal 1552  df-ex 1779  df-sb 2064  df-clab 2713  df-cleq 2726  df-dif 3934  df-nul 4314

This theorem is referenced by:  map0b  8905  disjen  9156  mapdom1  9164  pwxpndom2  10687  fzdisj  13573  smu01lem  16504  prmreclem5  16940  vdwap0  16996  natfval  17965  fucbas  17979  fuchom  17980  coafval  18080  efgval  19703  lsppratlem6  21122  lbsextlem4  21131  psrvscafval  21922  cfinufil  23882  ufinffr  23883  fin1aufil  23886  bldisj  24353  reconnlem1  24784  pcofval  24979  bcthlem5  25298  volfiniun  25518  fta1g  26145  fta1  26286  rpvmasum  27506  0ringprmidl  33412  0ringmon1p  33518  0ringirng  33676  unblimceq0  36467  bj-ab0  36868  bj-projval  36956  finxpnom  37361  ipo0  44425  ifr0  44426  limclner  45623