HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Theorem dtru 2762
Description: At least two sets exist (or in terms of first-order logic, the universe of discourse has two or more objects). Note that we may not substitute the same variable for both x and y (as indicated by the distinct variable requirement), for otherwise we would contradict stdpc6 1123. Assuming that ZF set theory is consistent, we cannot prove this theorem unless we specify that x and y be distinct. Specifically, theorem cla4ev 1860 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.

See dtruALT 2738 for a version proved without using ax-16 1206, ax-ext 1452, or ax-sep 2693.

Assertion
Ref Expression
dtru |- -. A.x x = y
Distinct variable group:   x,y
Proof of Theorem dtru
StepHypRef Expression
1 0inp0 2728 . . . 4 |- (y = (/) -> -. y = {(/)})
2 p0ex 2760 . . . . 5 |- {(/)} e. V
3 eqeq2 1476 . . . . . 6 |- (x = {(/)} -> (y = x <-> y = {(/)}))
43negbid 609 . . . . 5 |- (x = {(/)} -> (-. y = x <-> -. y = {(/)}))
52, 4cla4ev 1860 . . . 4 |- (-. y = {(/)} -> E.x -. y = x)
61, 5syl 10 . . 3 |- (y = (/) -> E.x -. y = x)
7 0ex 2701 . . . 4 |- (/) e. V
8 eqeq2 1476 . . . . 5 |- (x = (/) -> (y = x <-> y = (/)))
98negbid 609 . . . 4 |- (x = (/) -> (-. y = x <-> -. y = (/)))
107, 9cla4ev 1860 . . 3 |- (-. y = (/) -> E.x -. y = x)
116, 10pm2.61i 126 . 2 |- E.x -. y = x
12 exnal 1034 . . 3 |- (E.x -. y = x <-> -. A.x y = x)
13 eqcom 1469 . . . . 5 |- (y = x <-> x = y)
1413albii 996 . . . 4 |- (A.x y = x <-> A.x x = y)
1514negbii 187 . . 3 |- (-. A.x y = x <-> -. A.x x = y)
1612, 15bitr 173 . 2 |- (E.x -. y = x <-> -. A.x x = y)
1711, 16mpbi 189 1 |- -. A.x x = y
Colors of variables: wff set class
Syntax hints:  -. wn 2  A.wal 951   = wceq 953  E.wex 977  (/)c0 2270  {csn 2399
This theorem is referenced by:  dtrucor 2763  dvdemo1 2765  zfcndpow 4940
This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 959  ax-gen 960  ax-8 961  ax-10 963  ax-11 964  ax-12 965  ax-13 966  ax-14 967  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975  ax-9o 1119  ax-10o 1136  ax-16 1206  ax-11o 1213  ax-ext 1452  ax-sep 2693  ax-nul 2700  ax-pow 2732
This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 978  df-sb 1168  df-eu 1375  df-mo 1376  df-clab 1457  df-cleq 1462  df-clel 1465  df-ne 1579  df-v 1803  df-dif 2039  df-un 2040  df-in 2041  df-ss 2043  df-nul 2271  df-pw 2392  df-sn 2402  df-pr 2403
Copyright terms: Public domain