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

Theorem dtru 4382
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 1699.

This theorem is proved directly from set theory axioms (no set theory definitions) and does not use ax-ext 2416 or ax-sep 4322. See dtruALT 4388 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 4373 . . . . 5  |-  E. w  x  e.  w
2 ax-nul 4330 . . . . . 6  |-  E. z A. x  -.  x  e.  z
3 sp 1763 . . . . . 6  |-  ( A. x  -.  x  e.  z  ->  -.  x  e.  z )
42, 3eximii 1587 . . . . 5  |-  E. z  -.  x  e.  z
5 eeanv 1937 . . . . 5  |-  ( E. w E. z ( x  e.  w  /\  -.  x  e.  z
)  <->  ( E. w  x  e.  w  /\  E. z  -.  x  e.  z ) )
61, 4, 5mpbir2an 887 . . . 4  |-  E. w E. z ( x  e.  w  /\  -.  x  e.  z )
7 ax-14 1729 . . . . . . 7  |-  ( w  =  z  ->  (
x  e.  w  ->  x  e.  z )
)
87com12 29 . . . . . 6  |-  ( x  e.  w  ->  (
w  =  z  ->  x  e.  z )
)
98con3and 429 . . . . 5  |-  ( ( x  e.  w  /\  -.  x  e.  z
)  ->  -.  w  =  z )
1092eximi 1586 . . . 4  |-  ( E. w E. z ( x  e.  w  /\  -.  x  e.  z
)  ->  E. w E. z  -.  w  =  z )
116, 10ax-mp 8 . . 3  |-  E. w E. z  -.  w  =  z
12 equequ2 1698 . . . . . . 7  |-  ( z  =  y  ->  (
w  =  z  <->  w  =  y ) )
1312notbid 286 . . . . . 6  |-  ( z  =  y  ->  ( -.  w  =  z  <->  -.  w  =  y ) )
14 ax-8 1687 . . . . . . . 8  |-  ( x  =  w  ->  (
x  =  y  ->  w  =  y )
)
1514con3d 127 . . . . . . 7  |-  ( x  =  w  ->  ( -.  w  =  y  ->  -.  x  =  y ) )
1615spimev 1964 . . . . . 6  |-  ( -.  w  =  y  ->  E. x  -.  x  =  y )
1713, 16syl6bi 220 . . . . 5  |-  ( z  =  y  ->  ( -.  w  =  z  ->  E. x  -.  x  =  y ) )
18 ax-8 1687 . . . . . . . 8  |-  ( x  =  z  ->  (
x  =  y  -> 
z  =  y ) )
1918con3d 127 . . . . . . 7  |-  ( x  =  z  ->  ( -.  z  =  y  ->  -.  x  =  y ) )
2019spimev 1964 . . . . . 6  |-  ( -.  z  =  y  ->  E. x  -.  x  =  y )
2120a1d 23 . . . . 5  |-  ( -.  z  =  y  -> 
( -.  w  =  z  ->  E. x  -.  x  =  y
) )
2217, 21pm2.61i 158 . . . 4  |-  ( -.  w  =  z  ->  E. x  -.  x  =  y )
2322exlimivv 1645 . . 3  |-  ( E. w E. z  -.  w  =  z  ->  E. x  -.  x  =  y )
2411, 23ax-mp 8 . 2  |-  E. x  -.  x  =  y
25 exnal 1583 . 2  |-  ( E. x  -.  x  =  y  <->  -.  A. x  x  =  y )
2624, 25mpbi 200 1  |-  -.  A. x  x  =  y
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 359   A.wal 1549   E.wex 1550
This theorem is referenced by:  ax16b  4383  eunex  4384  nfnid  4385  dtrucor  4389  dvdemo1  4391  brprcneu  5712  zfcndpow  8480
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-13 1727  ax-14 1729  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-nul 4330  ax-pow 4369
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554
  Copyright terms: Public domain W3C validator