Description: Alternate proof of dtru which requires more axioms but is shorter and may be easier to understand. Like dtruALT2 , it uses ax-pow rather than ax-pr .
Assuming that ZF set theory is consistent, we cannot prove this theorem unless we specify that x and y be distinct. Specifically, Theorem spcev requires that x must not occur in the subexpression -. y = { (/) } in step 4 nor in the subexpression -. y = (/) in step 9. The proof verifier will require that x and y 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 | ||
|---|---|---|---|
| Assertion | dtruALT | ⊢ ¬ ∀ 𝑥 𝑥 = 𝑦 |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | 0inp0 | ⊢ ( 𝑦 = ∅ → ¬ 𝑦 = { ∅ } ) | |
| 2 | p0ex | ⊢ { ∅ } ∈ V | |
| 3 | eqeq2 | ⊢ ( 𝑥 = { ∅ } → ( 𝑦 = 𝑥 ↔ 𝑦 = { ∅ } ) ) | |
| 4 | 3 | notbid | ⊢ ( 𝑥 = { ∅ } → ( ¬ 𝑦 = 𝑥 ↔ ¬ 𝑦 = { ∅ } ) ) |
| 5 | 2 4 | spcev | ⊢ ( ¬ 𝑦 = { ∅ } → ∃ 𝑥 ¬ 𝑦 = 𝑥 ) |
| 6 | 1 5 | syl | ⊢ ( 𝑦 = ∅ → ∃ 𝑥 ¬ 𝑦 = 𝑥 ) |
| 7 | 0ex | ⊢ ∅ ∈ V | |
| 8 | eqeq2 | ⊢ ( 𝑥 = ∅ → ( 𝑦 = 𝑥 ↔ 𝑦 = ∅ ) ) | |
| 9 | 8 | notbid | ⊢ ( 𝑥 = ∅ → ( ¬ 𝑦 = 𝑥 ↔ ¬ 𝑦 = ∅ ) ) |
| 10 | 7 9 | spcev | ⊢ ( ¬ 𝑦 = ∅ → ∃ 𝑥 ¬ 𝑦 = 𝑥 ) |
| 11 | 6 10 | pm2.61i | ⊢ ∃ 𝑥 ¬ 𝑦 = 𝑥 |
| 12 | exnal | ⊢ ( ∃ 𝑥 ¬ 𝑦 = 𝑥 ↔ ¬ ∀ 𝑥 𝑦 = 𝑥 ) | |
| 13 | eqcom | ⊢ ( 𝑦 = 𝑥 ↔ 𝑥 = 𝑦 ) | |
| 14 | 13 | albii | ⊢ ( ∀ 𝑥 𝑦 = 𝑥 ↔ ∀ 𝑥 𝑥 = 𝑦 ) |
| 15 | 12 14 | xchbinx | ⊢ ( ∃ 𝑥 ¬ 𝑦 = 𝑥 ↔ ¬ ∀ 𝑥 𝑥 = 𝑦 ) |
| 16 | 11 15 | mpbi | ⊢ ¬ ∀ 𝑥 𝑥 = 𝑦 |