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

Theorem dtru 4607
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 1880.

This theorem is proved directly from set theory axioms (no set theory definitions) and does not use ax-ext 2441 or ax-sep 4538. See dtruALT 4645 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 4598 . . . 4  |-  E. w  x  e.  w
2 ax-nul 4547 . . . . 5  |-  E. z A. x  -.  x  e.  z
3 sp 1947 . . . . 5  |-  ( A. x  -.  x  e.  z  ->  -.  x  e.  z )
42, 3eximii 1719 . . . 4  |-  E. z  -.  x  e.  z
5 eeanv 2088 . . . 4  |-  ( E. w E. z ( x  e.  w  /\  -.  x  e.  z
)  <->  ( E. w  x  e.  w  /\  E. z  -.  x  e.  z ) )
61, 4, 5mpbir2an 936 . . 3  |-  E. w E. z ( x  e.  w  /\  -.  x  e.  z )
7 ax9 1910 . . . . . 6  |-  ( w  =  z  ->  (
x  e.  w  ->  x  e.  z )
)
87com12 32 . . . . 5  |-  ( x  e.  w  ->  (
w  =  z  ->  x  e.  z )
)
98con3dimp 447 . . . 4  |-  ( ( x  e.  w  /\  -.  x  e.  z
)  ->  -.  w  =  z )
1092eximi 1718 . . 3  |-  ( E. w E. z ( x  e.  w  /\  -.  x  e.  z
)  ->  E. w E. z  -.  w  =  z )
11 equequ2 1878 . . . . . . 7  |-  ( z  =  y  ->  (
w  =  z  <->  w  =  y ) )
1211notbid 300 . . . . . 6  |-  ( z  =  y  ->  ( -.  w  =  z  <->  -.  w  =  y ) )
13 ax7 1870 . . . . . . . 8  |-  ( x  =  w  ->  (
x  =  y  ->  w  =  y )
)
1413con3d 140 . . . . . . 7  |-  ( x  =  w  ->  ( -.  w  =  y  ->  -.  x  =  y ) )
1514spimev 2113 . . . . . 6  |-  ( -.  w  =  y  ->  E. x  -.  x  =  y )
1612, 15syl6bi 236 . . . . 5  |-  ( z  =  y  ->  ( -.  w  =  z  ->  E. x  -.  x  =  y ) )
17 ax7 1870 . . . . . . . 8  |-  ( x  =  z  ->  (
x  =  y  -> 
z  =  y ) )
1817con3d 140 . . . . . . 7  |-  ( x  =  z  ->  ( -.  z  =  y  ->  -.  x  =  y ) )
1918spimev 2113 . . . . . 6  |-  ( -.  z  =  y  ->  E. x  -.  x  =  y )
2019a1d 26 . . . . 5  |-  ( -.  z  =  y  -> 
( -.  w  =  z  ->  E. x  -.  x  =  y
) )
2116, 20pm2.61i 169 . . . 4  |-  ( -.  w  =  z  ->  E. x  -.  x  =  y )
2221exlimivv 1788 . . 3  |-  ( E. w E. z  -.  w  =  z  ->  E. x  -.  x  =  y )
236, 10, 22mp2b 10 . 2  |-  E. x  -.  x  =  y
24 exnal 1709 . 2  |-  ( E. x  -.  x  =  y  <->  -.  A. x  x  =  y )
2523, 24mpbi 213 1  |-  -.  A. x  x  =  y
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 375   A.wal 1452   E.wex 1673
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-6 1815  ax-7 1861  ax-8 1899  ax-9 1906  ax-10 1925  ax-11 1930  ax-12 1943  ax-13 2101  ax-nul 4547  ax-pow 4594
This theorem depends on definitions:  df-bi 190  df-an 377  df-tru 1457  df-ex 1674  df-nf 1678
This theorem is referenced by:  axc16b  4608  eunex  4609  nfnid  4642  dtrucor  4646  dvdemo1  4648  brprcneu  5880  zfcndpow  9066
  Copyright terms: Public domain W3C validator