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

Theorem dtruALT 5392
Description: Alternate proof of dtru 5442 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 3595 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 5363 . . . 4 (𝑦 = ∅ → ¬ 𝑦 = {∅})
2 p0ex 5388 . . . . 5 {∅} ∈ V
3 eqeq2 2740 . . . . . 6 (𝑥 = {∅} → (𝑦 = 𝑥𝑦 = {∅}))
43notbid 317 . . . . 5 (𝑥 = {∅} → (¬ 𝑦 = 𝑥 ↔ ¬ 𝑦 = {∅}))
52, 4spcev 3595 . . . 4 𝑦 = {∅} → ∃𝑥 ¬ 𝑦 = 𝑥)
61, 5syl 17 . . 3 (𝑦 = ∅ → ∃𝑥 ¬ 𝑦 = 𝑥)
7 0ex 5311 . . . 4 ∅ ∈ V
8 eqeq2 2740 . . . . 5 (𝑥 = ∅ → (𝑦 = 𝑥𝑦 = ∅))
98notbid 317 . . . 4 (𝑥 = ∅ → (¬ 𝑦 = 𝑥 ↔ ¬ 𝑦 = ∅))
107, 9spcev 3595 . . 3 𝑦 = ∅ → ∃𝑥 ¬ 𝑦 = 𝑥)
116, 10pm2.61i 182 . 2 𝑥 ¬ 𝑦 = 𝑥
12 exnal 1821 . . 3 (∃𝑥 ¬ 𝑦 = 𝑥 ↔ ¬ ∀𝑥 𝑦 = 𝑥)
13 eqcom 2735 . . . 4 (𝑦 = 𝑥𝑥 = 𝑦)
1413albii 1813 . . 3 (∀𝑥 𝑦 = 𝑥 ↔ ∀𝑥 𝑥 = 𝑦)
1512, 14xchbinx 333 . 2 (∃𝑥 ¬ 𝑦 = 𝑥 ↔ ¬ ∀𝑥 𝑥 = 𝑦)
1611, 15mpbi 229 1 ¬ ∀𝑥 𝑥 = 𝑦
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wal 1531   = wceq 1533  wex 1773  c0 4326  {csn 4632
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 2699  ax-sep 5303  ax-nul 5310  ax-pow 5369
This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-clab 2706  df-cleq 2720  df-clel 2806  df-ne 2938  df-v 3475  df-dif 3952  df-in 3956  df-ss 3966  df-nul 4327  df-pw 4608  df-sn 4633
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator