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

Theorem 2eu8 2391
 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 2390. (Contributed by NM, 20-Feb-2005.)
Assertion
Ref Expression
2eu8

Proof of Theorem 2eu8
StepHypRef Expression
1 2eu2 2385 . . 3
21pm5.32i 643 . 2
3 nfeu1 2311 . . . . 5
43nfeu 2317 . . . 4
54euan 2361 . . 3
6 ancom 452 . . . . . 6
76eubii 2323 . . . . 5
8 nfe1 1920 . . . . . 6
98euan 2361 . . . . 5
10 ancom 452 . . . . 5
117, 9, 103bitri 275 . . . 4
1211eubii 2323 . . 3
13 ancom 452 . . 3
145, 12, 133bitr4ri 282 . 2
15 2eu7 2390 . 2
162, 14, 153bitr3ri 280 1
 Colors of variables: wff setvar class Syntax hints:   wb 188   wa 371  wex 1665  weu 2301 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1671  ax-4 1684  ax-5 1760  ax-6 1807  ax-7 1853  ax-10 1917  ax-11 1922  ax-12 1935  ax-13 2093 This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-tru 1449  df-ex 1666  df-nf 1670  df-eu 2305  df-mo 2306 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator