Theorem eq0rdv 4339

Description: Deduction for equality to the empty set. (Contributed by NM, 11-Jul-2014.) Avoid ax-8 2109, df-clel 2817. (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 1931	. 2 ⊢ (𝜑 → ∀𝑥 ¬ 𝑥 ∈ 𝐴)
3		dfnul4 4259	. . . 4 ⊢ ∅ = {𝑦 ∣ ⊥}
4	3	eqeq2i 2752	. . 3 ⊢ (𝐴 = ∅ ↔ 𝐴 = {𝑦 ∣ ⊥})
5		dfcleq 2732	. . 3 ⊢ (𝐴 = {𝑦 ∣ ⊥} ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ {𝑦 ∣ ⊥}))
6		df-clab 2717	. . . . . . 7 ⊢ (𝑥 ∈ {𝑦 ∣ ⊥} ↔ [𝑥 / 𝑦]⊥)
7		sbv 2092	. . . . . . 7 ⊢ ([𝑥 / 𝑦]⊥ ↔ ⊥)
8	6, 7	bitri 274	. . . . . 6 ⊢ (𝑥 ∈ {𝑦 ∣ ⊥} ↔ ⊥)
9	8	bibi2i 338	. . . . 5 ⊢ ((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ {𝑦 ∣ ⊥}) ↔ (𝑥 ∈ 𝐴 ↔ ⊥))
10	9	albii 1822	. . . 4 ⊢ (∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ {𝑦 ∣ ⊥}) ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ ⊥))
11		nbfal 1554	. . . . . 6 ⊢ (¬ 𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐴 ↔ ⊥))
12	11	bicomi 223	. . . . 5 ⊢ ((𝑥 ∈ 𝐴 ↔ ⊥) ↔ ¬ 𝑥 ∈ 𝐴)
13	12	albii 1822	. . . 4 ⊢ (∀𝑥(𝑥 ∈ 𝐴 ↔ ⊥) ↔ ∀𝑥 ¬ 𝑥 ∈ 𝐴)
14	10, 13	bitri 274	. . 3 ⊢ (∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ {𝑦 ∣ ⊥}) ↔ ∀𝑥 ¬ 𝑥 ∈ 𝐴)
15	4, 5, 14	3bitrri 298	. 2 ⊢ (∀𝑥 ¬ 𝑥 ∈ 𝐴 ↔ 𝐴 = ∅)
16	2, 15	sylib 217	1 ⊢ (𝜑 → 𝐴 = ∅)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205  ∀wal 1537   = wceq 1539  ⊥wfal 1551  [wsb 2068   ∈ wcel 2107  {cab 2716  ∅c0 4257

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-dif 3891  df-nul 4258

This theorem is referenced by:  map0b  8680  disjen  8930  mapdom1  8938  pwxpndom2  10430  fzdisj  13292  smu01lem  16201  prmreclem5  16630  vdwap0  16686  natfval  17671  fucbas  17686  fuchom  17687  fuchomOLD  17688  coafval  17788  efgval  19332  lsppratlem6  20423  lbsextlem4  20432  psrvscafval  21168  cfinufil  23088  ufinffr  23089  fin1aufil  23092  bldisj  23560  reconnlem1  23998  pcofval  24182  bcthlem5  24501  volfiniun  24720  fta1g  25341  fta1  25477  rpvmasum  26683  0ringprmidl  31634  unblimceq0  34696  bj-ab0  35102  bj-projval  35195  finxpnom  35581  ipo0  42074  ifr0  42075  limclner  43199