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  8876  disjen  9133  mapdom1  9141  pwxpndom2  10659  fzdisj  13527  smu01lem  16425  prmreclem5  16852  vdwap0  16908  natfval  17896  fucbas  17911  fuchom  17912  fuchomOLD  17913  coafval  18013  efgval  19584  lsppratlem6  20764  lbsextlem4  20773  psrvscafval  21508  cfinufil  23431  ufinffr  23432  fin1aufil  23435  bldisj  23903  reconnlem1  24341  pcofval  24525  bcthlem5  24844  volfiniun  25063  fta1g  25684  fta1  25820  rpvmasum  27026  0ringprmidl  32563  0ringmon1p  32631  0ringirng  32748  unblimceq0  35378  bj-ab0  35783  bj-projval  35872  finxpnom  36277  ipo0  43198  ifr0  43199  limclner  44357