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

Theorem 2eu8 2243
 Description: Two equivalent expressions for double existential uniqueness. Curiously, we can put on either of the internal conjuncts but not both. We can also commute using 2eu7 2242. (Contributed by NM, 20-Feb-2005.)
Assertion
Ref Expression
2eu8

Proof of Theorem 2eu8
StepHypRef Expression
1 2eu2 2237 . . 3
21pm5.32i 618 . 2
3 nfeu1 2166 . . . . 5
43nfeu 2172 . . . 4
54euan 2213 . . 3
6 ancom 437 . . . . . 6
76eubii 2165 . . . . 5
8 nfe1 1718 . . . . . 6
98euan 2213 . . . . 5
10 ancom 437 . . . . 5
117, 9, 103bitri 262 . . . 4
1211eubii 2165 . . 3
13 ancom 437 . . 3
145, 12, 133bitr4ri 269 . 2
15 2eu7 2242 . 2
162, 14, 153bitr3ri 267 1
 Colors of variables: wff set class Syntax hints:   wb 176   wa 358  wex 1531  weu 2156 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878 This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-eu 2160  df-mo 2161
 Copyright terms: Public domain W3C validator