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

Theorem eq0rdv 4365
Description: Deduction for equality to the empty set. (Contributed by NM, 11-Jul-2014.) Avoid ax-8 2109, df-clel 2811. (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.
StepHypRef Expression
1 eq0rdv.1 . . 3 (𝜑 → ¬ 𝑥𝐴)
21alrimiv 1931 . 2 (𝜑 → ∀𝑥 ¬ 𝑥𝐴)
3 dfnul4 4285 . . . 4 ∅ = {𝑦 ∣ ⊥}
43eqeq2i 2746 . . 3 (𝐴 = ∅ ↔ 𝐴 = {𝑦 ∣ ⊥})
5 dfcleq 2726 . . 3 (𝐴 = {𝑦 ∣ ⊥} ↔ ∀𝑥(𝑥𝐴𝑥 ∈ {𝑦 ∣ ⊥}))
6 df-clab 2711 . . . . . . 7 (𝑥 ∈ {𝑦 ∣ ⊥} ↔ [𝑥 / 𝑦]⊥)
7 sbv 2092 . . . . . . 7 ([𝑥 / 𝑦]⊥ ↔ ⊥)
86, 7bitri 275 . . . . . 6 (𝑥 ∈ {𝑦 ∣ ⊥} ↔ ⊥)
98bibi2i 338 . . . . 5 ((𝑥𝐴𝑥 ∈ {𝑦 ∣ ⊥}) ↔ (𝑥𝐴 ↔ ⊥))
109albii 1822 . . . 4 (∀𝑥(𝑥𝐴𝑥 ∈ {𝑦 ∣ ⊥}) ↔ ∀𝑥(𝑥𝐴 ↔ ⊥))
11 nbfal 1557 . . . . . 6 𝑥𝐴 ↔ (𝑥𝐴 ↔ ⊥))
1211bicomi 223 . . . . 5 ((𝑥𝐴 ↔ ⊥) ↔ ¬ 𝑥𝐴)
1312albii 1822 . . . 4 (∀𝑥(𝑥𝐴 ↔ ⊥) ↔ ∀𝑥 ¬ 𝑥𝐴)
1410, 13bitri 275 . . 3 (∀𝑥(𝑥𝐴𝑥 ∈ {𝑦 ∣ ⊥}) ↔ ∀𝑥 ¬ 𝑥𝐴)
154, 5, 143bitrri 298 . 2 (∀𝑥 ¬ 𝑥𝐴𝐴 = ∅)
162, 15sylib 217 1 (𝜑𝐴 = ∅)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wal 1540   = wceq 1542  wfal 1554  [wsb 2068  wcel 2107  {cab 2710  c0 4283
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 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-dif 3914  df-nul 4284
This theorem is referenced by:  map0b  8824  disjen  9081  mapdom1  9089  pwxpndom2  10606  fzdisj  13474  smu01lem  16370  prmreclem5  16797  vdwap0  16853  natfval  17838  fucbas  17853  fuchom  17854  fuchomOLD  17855  coafval  17955  efgval  19504  lsppratlem6  20629  lbsextlem4  20638  psrvscafval  21374  cfinufil  23295  ufinffr  23296  fin1aufil  23299  bldisj  23767  reconnlem1  24205  pcofval  24389  bcthlem5  24708  volfiniun  24927  fta1g  25548  fta1  25684  rpvmasum  26890  0ringprmidl  32270  0ringmon1p  32312  0ringirng  32420  unblimceq0  35016  bj-ab0  35421  bj-projval  35513  finxpnom  35918  ipo0  42817  ifr0  42818  limclner  43978
  Copyright terms: Public domain W3C validator