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

Theorem dtruALT 5184
 Description: Alternate proof of dtru 5167 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 3549 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 5155 . . . 4 (𝑦 = ∅ → ¬ 𝑦 = {∅})
2 p0ex 5180 . . . . 5 {∅} ∈ V
3 eqeq2 2806 . . . . . 6 (𝑥 = {∅} → (𝑦 = 𝑥𝑦 = {∅}))
43notbid 319 . . . . 5 (𝑥 = {∅} → (¬ 𝑦 = 𝑥 ↔ ¬ 𝑦 = {∅}))
52, 4spcev 3549 . . . 4 𝑦 = {∅} → ∃𝑥 ¬ 𝑦 = 𝑥)
61, 5syl 17 . . 3 (𝑦 = ∅ → ∃𝑥 ¬ 𝑦 = 𝑥)
7 0ex 5107 . . . 4 ∅ ∈ V
8 eqeq2 2806 . . . . 5 (𝑥 = ∅ → (𝑦 = 𝑥𝑦 = ∅))
98notbid 319 . . . 4 (𝑥 = ∅ → (¬ 𝑦 = 𝑥 ↔ ¬ 𝑦 = ∅))
107, 9spcev 3549 . . 3 𝑦 = ∅ → ∃𝑥 ¬ 𝑦 = 𝑥)
116, 10pm2.61i 183 . 2 𝑥 ¬ 𝑦 = 𝑥
12 exnal 1808 . . 3 (∃𝑥 ¬ 𝑦 = 𝑥 ↔ ¬ ∀𝑥 𝑦 = 𝑥)
13 eqcom 2802 . . . 4 (𝑦 = 𝑥𝑥 = 𝑦)
1413albii 1801 . . 3 (∀𝑥 𝑦 = 𝑥 ↔ ∀𝑥 𝑥 = 𝑦)
1512, 14xchbinx 335 . 2 (∃𝑥 ¬ 𝑦 = 𝑥 ↔ ¬ ∀𝑥 𝑥 = 𝑦)
1611, 15mpbi 231 1 ¬ ∀𝑥 𝑥 = 𝑦
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3  ∀wal 1520   = wceq 1522  ∃wex 1761  ∅c0 4215  {csn 4476 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-ext 2769  ax-sep 5099  ax-nul 5106  ax-pow 5162 This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-ne 2985  df-v 3439  df-dif 3866  df-in 3870  df-ss 3878  df-nul 4216  df-pw 4459  df-sn 4477 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator