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

Theorem dtru 4558
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 1855.

This theorem is proved directly from set theory axioms (no set theory definitions) and does not use ax-ext 2408 or ax-sep 4489. See dtruALT 4596 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 4549 . . . 4  |-  E. w  x  e.  w
2 ax-nul 4498 . . . . 5  |-  E. z A. x  -.  x  e.  z
3 sp 1914 . . . . 5  |-  ( A. x  -.  x  e.  z  ->  -.  x  e.  z )
42, 3eximii 1703 . . . 4  |-  E. z  -.  x  e.  z
5 eeanv 2053 . . . 4  |-  ( E. w E. z ( x  e.  w  /\  -.  x  e.  z
)  <->  ( E. w  x  e.  w  /\  E. z  -.  x  e.  z ) )
61, 4, 5mpbir2an 928 . . 3  |-  E. w E. z ( x  e.  w  /\  -.  x  e.  z )
7 ax-9 1876 . . . . . 6  |-  ( w  =  z  ->  (
x  e.  w  ->  x  e.  z )
)
87com12 32 . . . . 5  |-  ( x  e.  w  ->  (
w  =  z  ->  x  e.  z )
)
98con3dimp 442 . . . 4  |-  ( ( x  e.  w  /\  -.  x  e.  z
)  ->  -.  w  =  z )
1092eximi 1702 . . 3  |-  ( E. w E. z ( x  e.  w  /\  -.  x  e.  z
)  ->  E. w E. z  -.  w  =  z )
11 equequ2 1853 . . . . . . 7  |-  ( z  =  y  ->  (
w  =  z  <->  w  =  y ) )
1211notbid 295 . . . . . 6  |-  ( z  =  y  ->  ( -.  w  =  z  <->  -.  w  =  y ) )
13 ax-7 1843 . . . . . . . 8  |-  ( x  =  w  ->  (
x  =  y  ->  w  =  y )
)
1413con3d 138 . . . . . . 7  |-  ( x  =  w  ->  ( -.  w  =  y  ->  -.  x  =  y ) )
1514spimev 2075 . . . . . 6  |-  ( -.  w  =  y  ->  E. x  -.  x  =  y )
1612, 15syl6bi 231 . . . . 5  |-  ( z  =  y  ->  ( -.  w  =  z  ->  E. x  -.  x  =  y ) )
17 ax-7 1843 . . . . . . . 8  |-  ( x  =  z  ->  (
x  =  y  -> 
z  =  y ) )
1817con3d 138 . . . . . . 7  |-  ( x  =  z  ->  ( -.  z  =  y  ->  -.  x  =  y ) )
1918spimev 2075 . . . . . 6  |-  ( -.  z  =  y  ->  E. x  -.  x  =  y )
2019a1d 26 . . . . 5  |-  ( -.  z  =  y  -> 
( -.  w  =  z  ->  E. x  -.  x  =  y
) )
2116, 20pm2.61i 167 . . . 4  |-  ( -.  w  =  z  ->  E. x  -.  x  =  y )
2221exlimivv 1771 . . 3  |-  ( E. w E. z  -.  w  =  z  ->  E. x  -.  x  =  y )
236, 10, 22mp2b 10 . 2  |-  E. x  -.  x  =  y
24 exnal 1693 . 2  |-  ( E. x  -.  x  =  y  <->  -.  A. x  x  =  y )
2523, 24mpbi 211 1  |-  -.  A. x  x  =  y
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 370   A.wal 1435   E.wex 1657
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-8 1874  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2063  ax-nul 4498  ax-pow 4545
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1658  df-nf 1662
This theorem is referenced by:  axc16b  4559  eunex  4560  nfnid  4593  dtrucor  4597  dvdemo1  4599  brprcneu  5818  zfcndpow  8992
  Copyright terms: Public domain W3C validator