NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  2eu8 Unicode version

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

Proof of Theorem 2eu8
StepHypRef Expression
1 2eu2 2285 . . 3
21pm5.32i 618 . 2
3 nfeu1 2214 . . . . 5  F/
43nfeu 2220 . . . 4  F/
54euan 2261 . . 3
6 ancom 437 . . . . . 6
76eubii 2213 . . . . 5
8 nfe1 1732 . . . . . 6  F/
98euan 2261 . . . . 5
10 ancom 437 . . . . 5
117, 9, 103bitri 262 . . . 4
1211eubii 2213 . . 3
13 ancom 437 . . 3
145, 12, 133bitr4ri 269 . 2
15 2eu7 2290 . 2
162, 14, 153bitr3ri 267 1
Colors of variables: wff setvar class
Syntax hints:   wb 176   wa 358  wex 1541  weu 2204
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-eu 2208  df-mo 2209
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator