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

Theorem eq0rdv 4402
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 4322 . . . 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 4320
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 3949  df-nul 4321
This theorem is referenced by:  map0b  8865  disjen  9122  mapdom1  9130  pwxpndom2  10647  fzdisj  13515  smu01lem  16413  prmreclem5  16840  vdwap0  16896  natfval  17884  fucbas  17899  fuchom  17900  fuchomOLD  17901  coafval  18001  efgval  19569  lsppratlem6  20742  lbsextlem4  20751  psrvscafval  21480  cfinufil  23401  ufinffr  23402  fin1aufil  23405  bldisj  23873  reconnlem1  24311  pcofval  24495  bcthlem5  24814  volfiniun  25033  fta1g  25654  fta1  25790  rpvmasum  26996  0ringprmidl  32519  0ringmon1p  32581  0ringirng  32691  unblimceq0  35288  bj-ab0  35693  bj-projval  35782  finxpnom  36187  ipo0  43079  ifr0  43080  limclner  44240
  Copyright terms: Public domain W3C validator