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

Theorem dtru 4419
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 1701.

This theorem is proved directly from set theory axioms (no set theory definitions) and does not use ax-ext 2423 or ax-sep 4355. See dtruALT 4425 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. (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 4410 . . . . 5  |-  E. w  x  e.  w
2 ax-nul 4363 . . . . . 6  |-  E. z A. x  -.  x  e.  z
3 sp 1765 . . . . . 6  |-  ( A. x  -.  x  e.  z  ->  -.  x  e.  z )
42, 3eximii 1588 . . . . 5  |-  E. z  -.  x  e.  z
5 eeanv 1940 . . . . 5  |-  ( E. w E. z ( x  e.  w  /\  -.  x  e.  z
)  <->  ( E. w  x  e.  w  /\  E. z  -.  x  e.  z ) )
61, 4, 5mpbir2an 888 . . . 4  |-  E. w E. z ( x  e.  w  /\  -.  x  e.  z )
7 ax-14 1731 . . . . . . 7  |-  ( w  =  z  ->  (
x  e.  w  ->  x  e.  z )
)
87com12 30 . . . . . 6  |-  ( x  e.  w  ->  (
w  =  z  ->  x  e.  z )
)
98con3and 430 . . . . 5  |-  ( ( x  e.  w  /\  -.  x  e.  z
)  ->  -.  w  =  z )
1092eximi 1587 . . . 4  |-  ( E. w E. z ( x  e.  w  /\  -.  x  e.  z
)  ->  E. w E. z  -.  w  =  z )
116, 10ax-mp 5 . . 3  |-  E. w E. z  -.  w  =  z
12 equequ2 1700 . . . . . . 7  |-  ( z  =  y  ->  (
w  =  z  <->  w  =  y ) )
1312notbid 287 . . . . . 6  |-  ( z  =  y  ->  ( -.  w  =  z  <->  -.  w  =  y ) )
14 ax-8 1689 . . . . . . . 8  |-  ( x  =  w  ->  (
x  =  y  ->  w  =  y )
)
1514con3d 128 . . . . . . 7  |-  ( x  =  w  ->  ( -.  w  =  y  ->  -.  x  =  y ) )
1615spimev 1967 . . . . . 6  |-  ( -.  w  =  y  ->  E. x  -.  x  =  y )
1713, 16syl6bi 221 . . . . 5  |-  ( z  =  y  ->  ( -.  w  =  z  ->  E. x  -.  x  =  y ) )
18 ax-8 1689 . . . . . . . 8  |-  ( x  =  z  ->  (
x  =  y  -> 
z  =  y ) )
1918con3d 128 . . . . . . 7  |-  ( x  =  z  ->  ( -.  z  =  y  ->  -.  x  =  y ) )
2019spimev 1967 . . . . . 6  |-  ( -.  z  =  y  ->  E. x  -.  x  =  y )
2120a1d 24 . . . . 5  |-  ( -.  z  =  y  -> 
( -.  w  =  z  ->  E. x  -.  x  =  y
) )
2217, 21pm2.61i 159 . . . 4  |-  ( -.  w  =  z  ->  E. x  -.  x  =  y )
2322exlimivv 1646 . . 3  |-  ( E. w E. z  -.  w  =  z  ->  E. x  -.  x  =  y )
2411, 23ax-mp 5 . 2  |-  E. x  -.  x  =  y
25 exnal 1584 . 2  |-  ( E. x  -.  x  =  y  <->  -.  A. x  x  =  y )
2624, 25mpbi 201 1  |-  -.  A. x  x  =  y
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 360   A.wal 1550   E.wex 1551
This theorem is referenced by:  ax16b  4420  eunex  4421  nfnid  4422  dtrucor  4426  dvdemo1  4428  brprcneu  5750  zfcndpow  8522
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 1668  ax-8 1689  ax-13 1729  ax-14 1731  ax-6 1746  ax-7 1751  ax-11 1763  ax-12 1953  ax-nul 4363  ax-pow 4406
This theorem depends on definitions:  df-bi 179  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555
  Copyright terms: Public domain W3C validator