MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  eq0rdv Structured version   Visualization version   GIF version

Theorem eq0rdv 4413
Description: Deduction for equality to the empty set. (Contributed by NM, 11-Jul-2014.) Avoid ax-8 2108, df-clel 2814. (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.
StepHypRef Expression
1 eq0rdv.1 . . 3 (𝜑 → ¬ 𝑥𝐴)
21alrimiv 1925 . 2 (𝜑 → ∀𝑥 ¬ 𝑥𝐴)
3 dfnul4 4341 . . . 4 ∅ = {𝑦 ∣ ⊥}
43eqeq2i 2748 . . 3 (𝐴 = ∅ ↔ 𝐴 = {𝑦 ∣ ⊥})
5 dfcleq 2728 . . 3 (𝐴 = {𝑦 ∣ ⊥} ↔ ∀𝑥(𝑥𝐴𝑥 ∈ {𝑦 ∣ ⊥}))
6 df-clab 2713 . . . . . . 7 (𝑥 ∈ {𝑦 ∣ ⊥} ↔ [𝑥 / 𝑦]⊥)
7 sbv 2086 . . . . . . 7 ([𝑥 / 𝑦]⊥ ↔ ⊥)
86, 7bitri 275 . . . . . 6 (𝑥 ∈ {𝑦 ∣ ⊥} ↔ ⊥)
98bibi2i 337 . . . . 5 ((𝑥𝐴𝑥 ∈ {𝑦 ∣ ⊥}) ↔ (𝑥𝐴 ↔ ⊥))
109albii 1816 . . . 4 (∀𝑥(𝑥𝐴𝑥 ∈ {𝑦 ∣ ⊥}) ↔ ∀𝑥(𝑥𝐴 ↔ ⊥))
11 nbfal 1552 . . . . . 6 𝑥𝐴 ↔ (𝑥𝐴 ↔ ⊥))
1211bicomi 224 . . . . 5 ((𝑥𝐴 ↔ ⊥) ↔ ¬ 𝑥𝐴)
1312albii 1816 . . . 4 (∀𝑥(𝑥𝐴 ↔ ⊥) ↔ ∀𝑥 ¬ 𝑥𝐴)
1410, 13bitri 275 . . 3 (∀𝑥(𝑥𝐴𝑥 ∈ {𝑦 ∣ ⊥}) ↔ ∀𝑥 ¬ 𝑥𝐴)
154, 5, 143bitrri 298 . 2 (∀𝑥 ¬ 𝑥𝐴𝐴 = ∅)
162, 15sylib 218 1 (𝜑𝐴 = ∅)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wal 1535   = wceq 1537  wfal 1549  [wsb 2062  wcel 2106  {cab 2712  c0 4339
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-9 2116  ax-ext 2706
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-fal 1550  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-dif 3966  df-nul 4340
This theorem is referenced by:  map0b  8922  disjen  9173  mapdom1  9181  pwxpndom2  10703  fzdisj  13588  smu01lem  16519  prmreclem5  16954  vdwap0  17010  natfval  18001  fucbas  18016  fuchom  18017  fuchomOLD  18018  coafval  18118  efgval  19750  lsppratlem6  21172  lbsextlem4  21181  psrvscafval  21986  cfinufil  23952  ufinffr  23953  fin1aufil  23956  bldisj  24424  reconnlem1  24862  pcofval  25057  bcthlem5  25376  volfiniun  25596  fta1g  26224  fta1  26365  rpvmasum  27585  0ringprmidl  33457  0ringmon1p  33563  0ringirng  33704  unblimceq0  36490  bj-ab0  36891  bj-projval  36979  finxpnom  37384  ipo0  44445  ifr0  44446  limclner  45607
  Copyright terms: Public domain W3C validator