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

Theorem dtruALT 5379
Description: Alternate proof of dtru 5429 which requires more axioms but is shorter and may be easier to understand.

Assuming that ZF set theory is consistent, we cannot prove this theorem unless we specify that 𝑥 and 𝑦 be distinct. Specifically, Theorem spcev 3590 requires that 𝑥 must not occur in the subexpression ¬ 𝑦 = {∅} in step 4 nor in the subexpression ¬ 𝑦 = ∅ in step 9. The proof verifier will require that 𝑥 and 𝑦 be in a distinct variable group to ensure this. You can check this by deleting the $d statement in set.mm and rerunning the verifier, which will print a detailed explanation of the distinct variable violation. (Contributed by NM, 15-Jul-1994.) (Proof modification is discouraged.) (New usage is discouraged.)

Assertion
Ref Expression
dtruALT ¬ ∀𝑥 𝑥 = 𝑦
Distinct variable group:   𝑥,𝑦

Proof of Theorem dtruALT
StepHypRef Expression
1 0inp0 5350 . . . 4 (𝑦 = ∅ → ¬ 𝑦 = {∅})
2 p0ex 5375 . . . . 5 {∅} ∈ V
3 eqeq2 2738 . . . . . 6 (𝑥 = {∅} → (𝑦 = 𝑥𝑦 = {∅}))
43notbid 318 . . . . 5 (𝑥 = {∅} → (¬ 𝑦 = 𝑥 ↔ ¬ 𝑦 = {∅}))
52, 4spcev 3590 . . . 4 𝑦 = {∅} → ∃𝑥 ¬ 𝑦 = 𝑥)
61, 5syl 17 . . 3 (𝑦 = ∅ → ∃𝑥 ¬ 𝑦 = 𝑥)
7 0ex 5300 . . . 4 ∅ ∈ V
8 eqeq2 2738 . . . . 5 (𝑥 = ∅ → (𝑦 = 𝑥𝑦 = ∅))
98notbid 318 . . . 4 (𝑥 = ∅ → (¬ 𝑦 = 𝑥 ↔ ¬ 𝑦 = ∅))
107, 9spcev 3590 . . 3 𝑦 = ∅ → ∃𝑥 ¬ 𝑦 = 𝑥)
116, 10pm2.61i 182 . 2 𝑥 ¬ 𝑦 = 𝑥
12 exnal 1821 . . 3 (∃𝑥 ¬ 𝑦 = 𝑥 ↔ ¬ ∀𝑥 𝑦 = 𝑥)
13 eqcom 2733 . . . 4 (𝑦 = 𝑥𝑥 = 𝑦)
1413albii 1813 . . 3 (∀𝑥 𝑦 = 𝑥 ↔ ∀𝑥 𝑥 = 𝑦)
1512, 14xchbinx 334 . 2 (∃𝑥 ¬ 𝑦 = 𝑥 ↔ ¬ ∀𝑥 𝑥 = 𝑦)
1611, 15mpbi 229 1 ¬ ∀𝑥 𝑥 = 𝑦
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wal 1531   = wceq 1533  wex 1773  c0 4317  {csn 4623
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2697  ax-sep 5292  ax-nul 5299  ax-pow 5356
This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-clab 2704  df-cleq 2718  df-clel 2804  df-ne 2935  df-v 3470  df-dif 3946  df-in 3950  df-ss 3960  df-nul 4318  df-pw 4599  df-sn 4624
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator