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

Theorem dtru 4331
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 1694.

This theorem is proved directly from set theory axioms (no set theory definitions) and does not use ax-ext 2368 or ax-sep 4271. See dtruALT 4337 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 4322 . . . . 5  |-  E. w  x  e.  w
2 ax-nul 4279 . . . . . 6  |-  E. z A. x  -.  x  e.  z
3 sp 1755 . . . . . 6  |-  ( A. x  -.  x  e.  z  ->  -.  x  e.  z )
42, 3eximii 1584 . . . . 5  |-  E. z  -.  x  e.  z
5 eeanv 1926 . . . . 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 1721 . . . . . . 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 1583 . . . 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 1693 . . . . . . 7  |-  ( z  =  y  ->  (
w  =  z  <->  w  =  y ) )
1312notbid 286 . . . . . 6  |-  ( z  =  y  ->  ( -.  w  =  z  <->  -.  w  =  y ) )
14 ax-8 1682 . . . . . . . 8  |-  ( x  =  w  ->  (
x  =  y  ->  w  =  y )
)
1514con3d 127 . . . . . . 7  |-  ( x  =  w  ->  ( -.  w  =  y  ->  -.  x  =  y ) )
1615spimev 2033 . . . . . 6  |-  ( -.  w  =  y  ->  E. x  -.  x  =  y )
1713, 16syl6bi 220 . . . . 5  |-  ( z  =  y  ->  ( -.  w  =  z  ->  E. x  -.  x  =  y ) )
18 ax-8 1682 . . . . . . . 8  |-  ( x  =  z  ->  (
x  =  y  -> 
z  =  y ) )
1918con3d 127 . . . . . . 7  |-  ( x  =  z  ->  ( -.  z  =  y  ->  -.  x  =  y ) )
2019spimev 2033 . . . . . 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 1642 . . 3  |-  ( E. w E. z  -.  w  =  z  ->  E. x  -.  x  =  y )
2411, 23ax-mp 8 . 2  |-  E. x  -.  x  =  y
25 exnal 1580 . 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 1546   E.wex 1547
This theorem is referenced by:  eunex  4333  nfnid  4334  dtrucor  4338  dvdemo1  4340  brprcneu  5661  zfcndpow  8424
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-13 1719  ax-14 1721  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-nul 4279  ax-pow 4318
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551
  Copyright terms: Public domain W3C validator