Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > dtruALT | Structured version Visualization version GIF version |
Description: Alternate proof of dtru 5248
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 3511 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.) |
Ref | Expression |
---|---|
dtruALT | ⊢ ¬ ∀𝑥 𝑥 = 𝑦 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 0inp0 5235 | . . . 4 ⊢ (𝑦 = ∅ → ¬ 𝑦 = {∅}) | |
2 | p0ex 5262 | . . . . 5 ⊢ {∅} ∈ V | |
3 | eqeq2 2748 | . . . . . 6 ⊢ (𝑥 = {∅} → (𝑦 = 𝑥 ↔ 𝑦 = {∅})) | |
4 | 3 | notbid 321 | . . . . 5 ⊢ (𝑥 = {∅} → (¬ 𝑦 = 𝑥 ↔ ¬ 𝑦 = {∅})) |
5 | 2, 4 | spcev 3511 | . . . 4 ⊢ (¬ 𝑦 = {∅} → ∃𝑥 ¬ 𝑦 = 𝑥) |
6 | 1, 5 | syl 17 | . . 3 ⊢ (𝑦 = ∅ → ∃𝑥 ¬ 𝑦 = 𝑥) |
7 | 0ex 5185 | . . . 4 ⊢ ∅ ∈ V | |
8 | eqeq2 2748 | . . . . 5 ⊢ (𝑥 = ∅ → (𝑦 = 𝑥 ↔ 𝑦 = ∅)) | |
9 | 8 | notbid 321 | . . . 4 ⊢ (𝑥 = ∅ → (¬ 𝑦 = 𝑥 ↔ ¬ 𝑦 = ∅)) |
10 | 7, 9 | spcev 3511 | . . 3 ⊢ (¬ 𝑦 = ∅ → ∃𝑥 ¬ 𝑦 = 𝑥) |
11 | 6, 10 | pm2.61i 185 | . 2 ⊢ ∃𝑥 ¬ 𝑦 = 𝑥 |
12 | exnal 1834 | . . 3 ⊢ (∃𝑥 ¬ 𝑦 = 𝑥 ↔ ¬ ∀𝑥 𝑦 = 𝑥) | |
13 | eqcom 2743 | . . . 4 ⊢ (𝑦 = 𝑥 ↔ 𝑥 = 𝑦) | |
14 | 13 | albii 1827 | . . 3 ⊢ (∀𝑥 𝑦 = 𝑥 ↔ ∀𝑥 𝑥 = 𝑦) |
15 | 12, 14 | xchbinx 337 | . 2 ⊢ (∃𝑥 ¬ 𝑦 = 𝑥 ↔ ¬ ∀𝑥 𝑥 = 𝑦) |
16 | 11, 15 | mpbi 233 | 1 ⊢ ¬ ∀𝑥 𝑥 = 𝑦 |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ∀wal 1541 = wceq 1543 ∃wex 1787 ∅c0 4223 {csn 4527 |
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 2018 ax-8 2114 ax-9 2122 ax-ext 2708 ax-sep 5177 ax-nul 5184 ax-pow 5243 |
This theorem depends on definitions: df-bi 210 df-an 400 df-tru 1546 df-fal 1556 df-ex 1788 df-sb 2073 df-clab 2715 df-cleq 2728 df-clel 2809 df-ne 2933 df-v 3400 df-dif 3856 df-in 3860 df-ss 3870 df-nul 4224 df-pw 4501 df-sn 4528 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |