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

Theorem dtru 4201
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 1650.

This theorem is proved directly from set theory axioms (no set theory definitions) and does not use ax-ext 2264 or ax-sep 4141. See dtruALT 4207 for a shorter proof using these axioms.

The proof makes use of dummy variables  z and  w which do not appear in the final theorem. They must be distinct from each other and from  x and  y. In other words, if we were to substitute  x for  z throughout the proof, the proof would fail. Although this requirement is made explicitly in the set.mm source file, it is implicit on the web page (i.e. doesn't appear in the "Distinct variable group"). (Contributed by NM, 7-Nov-2006.)

Assertion
Ref Expression
dtru  |-  -.  A. x  x  =  y
Distinct variable group:    x, y

Proof of Theorem dtru
Dummy variables  w  z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 el 4192 . . . . 5  |-  E. w  x  e.  w
2 ax-nul 4149 . . . . . 6  |-  E. z A. x  -.  x  e.  z
3 sp 1716 . . . . . . 7  |-  ( A. x  -.  x  e.  z  ->  -.  x  e.  z )
43eximi 1563 . . . . . 6  |-  ( E. z A. x  -.  x  e.  z  ->  E. z  -.  x  e.  z )
52, 4ax-mp 8 . . . . 5  |-  E. z  -.  x  e.  z
6 eeanv 1854 . . . . 5  |-  ( E. w E. z ( x  e.  w  /\  -.  x  e.  z
)  <->  ( E. w  x  e.  w  /\  E. z  -.  x  e.  z ) )
71, 5, 6mpbir2an 886 . . . 4  |-  E. w E. z ( x  e.  w  /\  -.  x  e.  z )
8 ax-14 1688 . . . . . . 7  |-  ( w  =  z  ->  (
x  e.  w  ->  x  e.  z )
)
98com12 27 . . . . . 6  |-  ( x  e.  w  ->  (
w  =  z  ->  x  e.  z )
)
109con3and 428 . . . . 5  |-  ( ( x  e.  w  /\  -.  x  e.  z
)  ->  -.  w  =  z )
11102eximi 1564 . . . 4  |-  ( E. w E. z ( x  e.  w  /\  -.  x  e.  z
)  ->  E. w E. z  -.  w  =  z )
127, 11ax-mp 8 . . 3  |-  E. w E. z  -.  w  =  z
13 equequ2 1649 . . . . . . 7  |-  ( z  =  y  ->  (
w  =  z  <->  w  =  y ) )
1413notbid 285 . . . . . 6  |-  ( z  =  y  ->  ( -.  w  =  z  <->  -.  w  =  y ) )
15 ax-8 1643 . . . . . . . 8  |-  ( x  =  w  ->  (
x  =  y  ->  w  =  y )
)
1615con3d 125 . . . . . . 7  |-  ( x  =  w  ->  ( -.  w  =  y  ->  -.  x  =  y ) )
1716spimev 1939 . . . . . 6  |-  ( -.  w  =  y  ->  E. x  -.  x  =  y )
1814, 17syl6bi 219 . . . . 5  |-  ( z  =  y  ->  ( -.  w  =  z  ->  E. x  -.  x  =  y ) )
19 ax-8 1643 . . . . . . . 8  |-  ( x  =  z  ->  (
x  =  y  -> 
z  =  y ) )
2019con3d 125 . . . . . . 7  |-  ( x  =  z  ->  ( -.  z  =  y  ->  -.  x  =  y ) )
2120spimev 1939 . . . . . 6  |-  ( -.  z  =  y  ->  E. x  -.  x  =  y )
2221a1d 22 . . . . 5  |-  ( -.  z  =  y  -> 
( -.  w  =  z  ->  E. x  -.  x  =  y
) )
2318, 22pm2.61i 156 . . . 4  |-  ( -.  w  =  z  ->  E. x  -.  x  =  y )
2423exlimivv 1667 . . 3  |-  ( E. w E. z  -.  w  =  z  ->  E. x  -.  x  =  y )
2512, 24ax-mp 8 . 2  |-  E. x  -.  x  =  y
26 exnal 1561 . 2  |-  ( E. x  -.  x  =  y  <->  -.  A. x  x  =  y )
2725, 26mpbi 199 1  |-  -.  A. x  x  =  y
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 358   A.wal 1527   E.wex 1528    = wceq 1623    e. wcel 1684
This theorem is referenced by:  ax16b  4202  eunex  4203  nfnid  4204  dtrucor  4208  dvdemo1  4210  brprcneu  5518  zfcndpow  8238
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-13 1686  ax-14 1688  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-nul 4149  ax-pow 4188
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532
  Copyright terms: Public domain W3C validator