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

Theorem dtruALT 4399
 Description: A version of dtru 4393 ("two things exist") with a shorter proof that uses more axioms but 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 3045 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 4374 . . . 4
2 p0ex 4389 . . . . 5
3 eqeq2 2447 . . . . . 6
43notbid 287 . . . . 5
52, 4spcev 3045 . . . 4
61, 5syl 16 . . 3
7 0ex 4342 . . . 4
8 eqeq2 2447 . . . . 5
98notbid 287 . . . 4
107, 9spcev 3045 . . 3
116, 10pm2.61i 159 . 2
12 exnal 1584 . . 3
13 eqcom 2440 . . . 4
1413albii 1576 . . 3
1512, 14xchbinx 303 . 2
1611, 15mpbi 201 1
 Colors of variables: wff set class Syntax hints:   wn 3  wal 1550  wex 1551   wceq 1653  c0 3630  csn 3816 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-14 1730  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419  ax-sep 4333  ax-nul 4341  ax-pow 4380 This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-v 2960  df-dif 3325  df-in 3329  df-ss 3336  df-nul 3631  df-pw 3803  df-sn 3822
 Copyright terms: Public domain W3C validator