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

Theorem eq0rdv 4405
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 4325 . . . 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 4323
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 3952  df-nul 4324
This theorem is referenced by:  map0b  8877  disjen  9134  mapdom1  9142  pwxpndom2  10660  fzdisj  13528  smu01lem  16426  prmreclem5  16853  vdwap0  16909  natfval  17897  fucbas  17912  fuchom  17913  fuchomOLD  17914  coafval  18014  efgval  19585  lsppratlem6  20765  lbsextlem4  20774  psrvscafval  21509  cfinufil  23432  ufinffr  23433  fin1aufil  23436  bldisj  23904  reconnlem1  24342  pcofval  24526  bcthlem5  24845  volfiniun  25064  fta1g  25685  fta1  25821  rpvmasum  27029  0ringprmidl  32568  0ringmon1p  32636  0ringirng  32753  unblimceq0  35383  bj-ab0  35788  bj-projval  35877  finxpnom  36282  ipo0  43208  ifr0  43209  limclner  44367
  Copyright terms: Public domain W3C validator