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

Theorem dtruALT 4684
Description: Alternate proof of dtru 4643 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 3201 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 4624 . . . 4
2 p0ex 4639 . . . . 5
3 eqeq2 2472 . . . . . 6
43notbid 294 . . . . 5
52, 4spcev 3201 . . . 4
61, 5syl 16 . . 3
7 0ex 4582 . . . 4
8 eqeq2 2472 . . . . 5
98notbid 294 . . . 4
107, 9spcev 3201 . . 3
116, 10pm2.61i 164 . 2
12 exnal 1648 . . 3
13 eqcom 2466 . . . 4
1413albii 1640 . . 3
1512, 14xchbinx 310 . 2
1611, 15mpbi 208 1
Colors of variables: wff setvar class
Syntax hints:  -.wn 3  A.wal 1393  =wceq 1395  E.wex 1612   c0 3784  {csn 4029
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-9 1822  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-sep 4573  ax-nul 4581  ax-pow 4630
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-v 3111  df-dif 3478  df-in 3482  df-ss 3489  df-nul 3785  df-pw 4014  df-sn 4030
  Copyright terms: Public domain W3C validator