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

Theorem dtru 4643
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 and (as indicated by the distinct variable requirement), for otherwise we would contradict stdpc6 1800.

This theorem is proved directly from set theory axioms (no set theory definitions) and does not use ax-ext 2435 or ax-sep 4573. See dtruALT 4684 for a shorter proof using these axioms.

The proof makes use of dummy variables and which do not appear in the final theorem. They must be distinct from each other and from and . In other words, if we were to substitute for throughout the proof, the proof would fail. (Contributed by NM, 7-Nov-2006.)

Assertion
Ref Expression
dtru
Distinct variable group:   ,

Proof of Theorem dtru
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 el 4634 . . . 4
2 ax-nul 4581 . . . . 5
3 sp 1859 . . . . 5
42, 3eximii 1658 . . . 4
5 eeanv 1988 . . . 4
61, 4, 5mpbir2an 920 . . 3
7 ax-9 1822 . . . . . 6
87com12 31 . . . . 5
98con3dimp 441 . . . 4
1092eximi 1657 . . 3
11 equequ2 1799 . . . . . . 7
1211notbid 294 . . . . . 6
13 ax-7 1790 . . . . . . . 8
1413con3d 133 . . . . . . 7
1514spimev 2010 . . . . . 6
1612, 15syl6bi 228 . . . . 5
17 ax-7 1790 . . . . . . . 8
1817con3d 133 . . . . . . 7
1918spimev 2010 . . . . . 6
2019a1d 25 . . . . 5
2116, 20pm2.61i 164 . . . 4
2221exlimivv 1723 . . 3
236, 10, 22mp2b 10 . 2
24 exnal 1648 . 2
2523, 24mpbi 208 1
Colors of variables: wff setvar class
Syntax hints:  -.wn 3  ->wi 4  /\wa 369  A.wal 1393  E.wex 1612
This theorem is referenced by:  axc16b  4644  eunex  4645  nfnid  4681  dtrucor  4685  dvdemo1  4687  brprcneu  5864  zfcndpow  9015
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-8 1820  ax-9 1822  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-nul 4581  ax-pow 4630
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617
  Copyright terms: Public domain W3C validator