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 | |- -. A. x x = y |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | 0inp0 | |- ( y = (/) -> -. y = { (/) } ) |
|
| 2 | p0ex | |- { (/) } e. _V |
|
| 3 | eqeq2 | |- ( x = { (/) } -> ( y = x <-> y = { (/) } ) ) |
|
| 4 | 3 | notbid | |- ( x = { (/) } -> ( -. y = x <-> -. y = { (/) } ) ) |
| 5 | 2 4 | spcev | |- ( -. y = { (/) } -> E. x -. y = x ) |
| 6 | 1 5 | syl | |- ( y = (/) -> E. x -. y = x ) |
| 7 | 0ex | |- (/) e. _V |
|
| 8 | eqeq2 | |- ( x = (/) -> ( y = x <-> y = (/) ) ) |
|
| 9 | 8 | notbid | |- ( x = (/) -> ( -. y = x <-> -. y = (/) ) ) |
| 10 | 7 9 | spcev | |- ( -. y = (/) -> E. x -. y = x ) |
| 11 | 6 10 | pm2.61i | |- E. x -. y = x |
| 12 | exnal | |- ( E. x -. y = x <-> -. A. x y = x ) |
|
| 13 | eqcom | |- ( y = x <-> x = y ) |
|
| 14 | 13 | albii | |- ( A. x y = x <-> A. x x = y ) |
| 15 | 12 14 | xchbinx | |- ( E. x -. y = x <-> -. A. x x = y ) |
| 16 | 11 15 | mpbi | |- -. A. x x = y |