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

Theorem dtru 4644
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 1749.

This theorem is proved directly from set theory axioms (no set theory definitions) and does not use ax-ext 2445 or ax-sep 4574. See dtruALT 4685 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 4635 . . . . 5  |-  E. w  x  e.  w
2 ax-nul 4582 . . . . . 6  |-  E. z A. x  -.  x  e.  z
3 sp 1808 . . . . . 6  |-  ( A. x  -.  x  e.  z  ->  -.  x  e.  z )
42, 3eximii 1637 . . . . 5  |-  E. z  -.  x  e.  z
5 eeanv 1957 . . . . 5  |-  ( E. w E. z ( x  e.  w  /\  -.  x  e.  z
)  <->  ( E. w  x  e.  w  /\  E. z  -.  x  e.  z ) )
61, 4, 5mpbir2an 918 . . . 4  |-  E. w E. z ( x  e.  w  /\  -.  x  e.  z )
7 ax-9 1771 . . . . . . 7  |-  ( w  =  z  ->  (
x  e.  w  ->  x  e.  z )
)
87com12 31 . . . . . 6  |-  ( x  e.  w  ->  (
w  =  z  ->  x  e.  z )
)
98con3dimp 441 . . . . 5  |-  ( ( x  e.  w  /\  -.  x  e.  z
)  ->  -.  w  =  z )
1092eximi 1636 . . . 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 1748 . . . . . . 7  |-  ( z  =  y  ->  (
w  =  z  <->  w  =  y ) )
1312notbid 294 . . . . . 6  |-  ( z  =  y  ->  ( -.  w  =  z  <->  -.  w  =  y ) )
14 ax-7 1739 . . . . . . . 8  |-  ( x  =  w  ->  (
x  =  y  ->  w  =  y )
)
1514con3d 133 . . . . . . 7  |-  ( x  =  w  ->  ( -.  w  =  y  ->  -.  x  =  y ) )
1615spimev 1979 . . . . . 6  |-  ( -.  w  =  y  ->  E. x  -.  x  =  y )
1713, 16syl6bi 228 . . . . 5  |-  ( z  =  y  ->  ( -.  w  =  z  ->  E. x  -.  x  =  y ) )
18 ax-7 1739 . . . . . . . 8  |-  ( x  =  z  ->  (
x  =  y  -> 
z  =  y ) )
1918con3d 133 . . . . . . 7  |-  ( x  =  z  ->  ( -.  z  =  y  ->  -.  x  =  y ) )
2019spimev 1979 . . . . . 6  |-  ( -.  z  =  y  ->  E. x  -.  x  =  y )
2120a1d 25 . . . . 5  |-  ( -.  z  =  y  -> 
( -.  w  =  z  ->  E. x  -.  x  =  y
) )
2217, 21pm2.61i 164 . . . 4  |-  ( -.  w  =  z  ->  E. x  -.  x  =  y )
2322exlimivv 1699 . . 3  |-  ( E. w E. z  -.  w  =  z  ->  E. x  -.  x  =  y )
2411, 23ax-mp 5 . 2  |-  E. x  -.  x  =  y
25 exnal 1628 . 2  |-  ( E. x  -.  x  =  y  <->  -.  A. x  x  =  y )
2624, 25mpbi 208 1  |-  -.  A. x  x  =  y
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 369   A.wal 1377   E.wex 1596
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-nul 4582  ax-pow 4631
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600
This theorem is referenced by:  axc16b  4645  eunex  4646  nfnid  4682  dtrucor  4686  dvdemo1  4688  brprcneu  5865  zfcndpow  9006
  Copyright terms: Public domain W3C validator