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

Theorem eq0rdv 4319
Description: Deduction for equality to the empty set. (Contributed by NM, 11-Jul-2014.) Avoid ax-8 2112, df-clel 2816. (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 1935 . 2 (𝜑 → ∀𝑥 ¬ 𝑥𝐴)
3 dfnul4 4239 . . . 4 ∅ = {𝑦 ∣ ⊥}
43eqeq2i 2750 . . 3 (𝐴 = ∅ ↔ 𝐴 = {𝑦 ∣ ⊥})
5 dfcleq 2730 . . 3 (𝐴 = {𝑦 ∣ ⊥} ↔ ∀𝑥(𝑥𝐴𝑥 ∈ {𝑦 ∣ ⊥}))
6 df-clab 2715 . . . . . . 7 (𝑥 ∈ {𝑦 ∣ ⊥} ↔ [𝑥 / 𝑦]⊥)
7 sbv 2094 . . . . . . 7 ([𝑥 / 𝑦]⊥ ↔ ⊥)
86, 7bitri 278 . . . . . 6 (𝑥 ∈ {𝑦 ∣ ⊥} ↔ ⊥)
98bibi2i 341 . . . . 5 ((𝑥𝐴𝑥 ∈ {𝑦 ∣ ⊥}) ↔ (𝑥𝐴 ↔ ⊥))
109albii 1827 . . . 4 (∀𝑥(𝑥𝐴𝑥 ∈ {𝑦 ∣ ⊥}) ↔ ∀𝑥(𝑥𝐴 ↔ ⊥))
11 nbfal 1558 . . . . . 6 𝑥𝐴 ↔ (𝑥𝐴 ↔ ⊥))
1211bicomi 227 . . . . 5 ((𝑥𝐴 ↔ ⊥) ↔ ¬ 𝑥𝐴)
1312albii 1827 . . . 4 (∀𝑥(𝑥𝐴 ↔ ⊥) ↔ ∀𝑥 ¬ 𝑥𝐴)
1410, 13bitri 278 . . 3 (∀𝑥(𝑥𝐴𝑥 ∈ {𝑦 ∣ ⊥}) ↔ ∀𝑥 ¬ 𝑥𝐴)
154, 5, 143bitrri 301 . 2 (∀𝑥 ¬ 𝑥𝐴𝐴 = ∅)
162, 15sylib 221 1 (𝜑𝐴 = ∅)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 209  wal 1541   = wceq 1543  wfal 1555  [wsb 2070  wcel 2110  {cab 2714  c0 4237
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-9 2120  ax-ext 2708
This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1546  df-fal 1556  df-ex 1788  df-sb 2071  df-clab 2715  df-cleq 2729  df-dif 3869  df-nul 4238
This theorem is referenced by:  map0b  8564  disjen  8803  mapdom1  8811  pwxpndom2  10279  fzdisj  13139  smu01lem  16044  prmreclem5  16473  vdwap0  16529  natfval  17453  fucbas  17468  fuchom  17469  fuchomOLD  17470  coafval  17570  efgval  19107  lsppratlem6  20189  lbsextlem4  20198  psrvscafval  20915  cfinufil  22825  ufinffr  22826  fin1aufil  22829  bldisj  23296  reconnlem1  23723  pcofval  23907  bcthlem5  24225  volfiniun  24444  fta1g  25065  fta1  25201  rpvmasum  26407  0ringprmidl  31339  unblimceq0  34424  bj-ab0  34830  bj-projval  34923  finxpnom  35309  ipo0  41740  ifr0  41741  limclner  42867
  Copyright terms: Public domain W3C validator