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

Theorem dtru 4095
 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 1821. This theorem is proved directly from set theory axioms (no set theory definitions) and does not use ax-ext 2234 or ax-sep 4038. See dtruALT 4101 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. Although this requirement is made explicitly in the set.mm source file, it is implicit on the web page (i.e. doesn't appear in the "Distinct variable group"). (Contributed by NM, 7-Nov-2006.)
Assertion
Ref Expression
dtru
Distinct variable group:   ,

Proof of Theorem dtru
StepHypRef Expression
1 el 4086 . . . . 5
2 ax-nul 4046 . . . . . 6
3 ax-4 1692 . . . . . . 7
43eximi 1574 . . . . . 6
52, 4ax-mp 10 . . . . 5
6 eeanv 2055 . . . . 5
71, 5, 6mpbir2an 891 . . . 4
8 ax-14 1626 . . . . . . 7
98com12 29 . . . . . 6
109con3and 430 . . . . 5
11102eximi 1575 . . . 4
127, 11ax-mp 10 . . 3
13 equequ2 1830 . . . . . . 7
1413notbid 287 . . . . . 6
15 ax-8 1623 . . . . . . . 8
1615con3d 127 . . . . . . 7
1716a4imev 1997 . . . . . 6
1814, 17syl6bi 221 . . . . 5
19 ax-8 1623 . . . . . . . 8
2019con3d 127 . . . . . . 7
2120a4imev 1997 . . . . . 6
2221a1d 24 . . . . 5
2318, 22pm2.61i 158 . . . 4
2423exlimivv 2025 . . 3
2512, 24ax-mp 10 . 2
26 exnal 1572 . 2
2725, 26mpbi 201 1
 Colors of variables: wff set class Syntax hints:   wn 5   wi 6   wa 360  wal 1532  wex 1537   wceq 1619   wcel 1621 This theorem is referenced by:  ax16b  4096  eunex  4097  nfnid  4098  dtrucor  4102  dvdemo1  4104  zfcndpow  8118 This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-13 1625  ax-14 1626  ax-17 1628  ax-9 1684  ax-4 1692  ax-nul 4046  ax-pow 4082 This theorem depends on definitions:  df-bi 179  df-an 362  df-tru 1315  df-ex 1538  df-nf 1540
 Copyright terms: Public domain W3C validator