ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  euotd Structured version   Unicode version

Theorem euotd 3982
Description: Prove existential uniqueness for an ordered triple. (Contributed by Mario Carneiro, 20-May-2015.)
Hypotheses
Ref Expression
euotd.1  _V
euotd.2  _V
euotd.3  C  _V
euotd.4  a  b  c  C
Assertion
Ref Expression
euotd  a b c  <. a ,  b ,  c
>.
Distinct variable groups:    a, b, c,,   , a,
b, c,    C, a, b, c,   , a,
b, c,
Allowed substitution hints:   (, a, b, c)

Proof of Theorem euotd
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 euotd.1 . . . 4  _V
2 euotd.2 . . . 4  _V
3 euotd.3 . . . 4  C  _V
4 otexg 3958 . . . 4  _V  _V  C  _V  <. ,  ,  C >.  _V
51, 2, 3, 4syl3anc 1134 . . 3  <. ,  ,  C >.  _V
6 euotd.4 . . . . . . . . . . . . 13  a  b  c  C
76biimpa 280 . . . . . . . . . . . 12  a  b  c  C
8 vex 2554 . . . . . . . . . . . . 13  a 
_V
9 vex 2554 . . . . . . . . . . . . 13  b 
_V
10 vex 2554 . . . . . . . . . . . . 13  c 
_V
118, 9, 10otth 3970 . . . . . . . . . . . 12  <. a ,  b ,  c
>.  <. ,  ,  C >.  a  b  c  C
127, 11sylibr 137 . . . . . . . . . . 11  <. a ,  b ,  c >.  <. ,  ,  C >.
1312eqeq2d 2048 . . . . . . . . . 10  <. a ,  b ,  c
>.  <. ,  ,  C >.
1413biimpd 132 . . . . . . . . 9  <. a ,  b ,  c
>.  <. ,  ,  C >.
1514impancom 247 . . . . . . . 8  <. a ,  b ,  c
>.  <. ,  ,  C >.
1615expimpd 345 . . . . . . 7 
<. a ,  b ,  c >.  <. ,  ,  C >.
1716exlimdv 1697 . . . . . 6  c  <. a ,  b ,  c
>.  <. ,  ,  C >.
1817exlimdvv 1774 . . . . 5  a b c  <. a ,  b ,  c
>.  <. ,  ,  C >.
19 tru 1246 . . . . . . . . . . 11
202adantr 261 . . . . . . . . . . . . 13  a  _V
213ad2antrr 457 . . . . . . . . . . . . . 14  a  b  C  _V
22 simpr 103 . . . . . . . . . . . . . . . . . . 19  a  b  c  C  a  b  c  C
2322, 11sylibr 137 . . . . . . . . . . . . . . . . . 18  a  b  c  C  <. a ,  b ,  c >.  <. ,  ,  C >.
2423eqcomd 2042 . . . . . . . . . . . . . . . . 17  a  b  c  C  <. ,  ,  C >.  <. a ,  b ,  c
>.
256biimpar 281 . . . . . . . . . . . . . . . . 17  a  b  c  C
2624, 25jca 290 . . . . . . . . . . . . . . . 16  a  b  c  C  <. ,  ,  C >.  <. a ,  b ,  c
>.
27 a1tru 1258 . . . . . . . . . . . . . . . 16  a  b  c  C
2826, 272thd 164 . . . . . . . . . . . . . . 15  a  b  c  C  <. ,  ,  C >.  <. a ,  b ,  c
>.
29283anassrs 1125 . . . . . . . . . . . . . 14  a  b  c  C  <. ,  ,  C >.  <. a ,  b ,  c >.
3021, 29sbcied 2793 . . . . . . . . . . . . 13  a  b  [. C  c ]. <. ,  ,  C >.  <. a ,  b ,  c
>.
3120, 30sbcied 2793 . . . . . . . . . . . 12  a  [.  b ]. [. C  c ]. <. ,  ,  C >.  <. a ,  b ,  c >.
321, 31sbcied 2793 . . . . . . . . . . 11  [.  a ]. [.  b ]. [. C  c ]. <. ,  ,  C >. 
<. a ,  b ,  c >.
3319, 32mpbiri 157 . . . . . . . . . 10  [.  a ]. [.  b ]. [. C  c ]. <. ,  ,  C >.  <. a ,  b ,  c
>.
3433spesbcd 2838 . . . . . . . . 9  a [.  b ]. [. C  c ]. <. ,  ,  C >.  <. a ,  b ,  c >.
35 nfcv 2175 . . . . . . . . . 10  F/_ b
36 nfsbc1v 2776 . . . . . . . . . . 11  F/ b
[.  b ]. [. C  c ]. <. ,  ,  C >.  <. a ,  b ,  c
>.
3736nfex 1525 . . . . . . . . . 10  F/ b a [.  b ]. [. C  c ]. <. ,  ,  C >.  <. a ,  b ,  c >.
38 sbceq1a 2767 . . . . . . . . . . 11  b  [. C  c ]. <. ,  ,  C >.  <. a ,  b ,  c
>.  [.  b ]. [. C  c ]. <. ,  ,  C >.  <. a ,  b ,  c >.
3938exbidv 1703 . . . . . . . . . 10  b  a [. C  c ]. <. ,  ,  C >. 
<. a ,  b ,  c >.  a [.  b ]. [. C  c ]. <. ,  ,  C >. 
<. a ,  b ,  c >.
4035, 37, 39spcegf 2630 . . . . . . . . 9  _V  a [.  b ]. [. C  c ]. <. ,  ,  C >. 
<. a ,  b ,  c >.  b a [. C  c ]. <. ,  ,  C >.  <. a ,  b ,  c
>.
412, 34, 40sylc 56 . . . . . . . 8  b a [. C  c ]. <. ,  ,  C >.  <. a ,  b ,  c
>.
42 nfcv 2175 . . . . . . . . 9  F/_ c C
43 nfsbc1v 2776 . . . . . . . . . . 11  F/ c
[. C  c ]. <. ,  ,  C >.  <. a ,  b ,  c
>.
4443nfex 1525 . . . . . . . . . 10  F/ c a [. C  c ]. <. ,  ,  C >.  <. a ,  b ,  c >.
4544nfex 1525 . . . . . . . . 9  F/ c b a [. C  c ]. <. ,  ,  C >.  <. a ,  b ,  c
>.
46 sbceq1a 2767 . . . . . . . . . 10  c  C  <. ,  ,  C >.  <. a ,  b ,  c
>.  [. C  c ]. <. ,  ,  C >.  <. a ,  b ,  c >.
47462exbidv 1745 . . . . . . . . 9  c  C  b a
<. ,  ,  C >.  <. a ,  b ,  c
>.  b a [. C  c ]. <. ,  ,  C >. 
<. a ,  b ,  c >.
4842, 45, 47spcegf 2630 . . . . . . . 8  C  _V  b a [. C  c ]. <. ,  ,  C >.  <. a ,  b ,  c
>.  c b a <. ,  ,  C >. 
<. a ,  b ,  c >.
493, 41, 48sylc 56 . . . . . . 7  c b a <. ,  ,  C >. 
<. a ,  b ,  c >.
50 excom13 1576 . . . . . . 7  c b a <. ,  ,  C >.  <. a ,  b ,  c
>.  a b c
<. ,  ,  C >.  <. a ,  b ,  c
>.
5149, 50sylib 127 . . . . . 6  a b c <. ,  ,  C >. 
<. a ,  b ,  c >.
52 eqeq1 2043 . . . . . . . 8  <. ,  ,  C >.  <. a ,  b ,  c >.  <. ,  ,  C >.  <. a ,  b ,  c
>.
5352anbi1d 438 . . . . . . 7  <. ,  ,  C >.  <. a ,  b ,  c
>.  <. ,  ,  C >.  <. a ,  b ,  c >.
54533exbidv 1746 . . . . . 6  <. ,  ,  C >.  a b c 
<. a ,  b ,  c >.  a b c <. ,  ,  C >. 
<. a ,  b ,  c >.
5551, 54syl5ibrcom 146 . . . . 5  <. ,  ,  C >.  a b c  <. a ,  b ,  c
>.
5618, 55impbid 120 . . . 4  a b c  <. a ,  b ,  c
>. 
<. ,  ,  C >.
5756alrimiv 1751 . . 3  a b c  <. a ,  b ,  c
>. 
<. ,  ,  C >.
58 eqeq2 2046 . . . . . 6  <. ,  ,  C >. 
<. ,  ,  C >.
5958bibi2d 221 . . . . 5  <. ,  ,  C >.  a b c 
<. a ,  b ,  c >.  a b c 
<. a ,  b ,  c >.  <. ,  ,  C >.
6059albidv 1702 . . . 4  <. ,  ,  C >.  a b c  <. a ,  b ,  c
>.  a b c 
<. a ,  b ,  c >.  <. ,  ,  C >.
6160spcegv 2635 . . 3  <. ,  ,  C >.  _V  a b c  <. a ,  b ,  c
>. 
<. ,  ,  C >.  a b c  <. a ,  b ,  c
>.
625, 57, 61sylc 56 . 2  a b c 
<. a ,  b ,  c >.
63 df-eu 1900 . 2  a b c  <. a ,  b ,  c
>.  a b c  <. a ,  b ,  c
>.
6462, 63sylibr 137 1  a b c  <. a ,  b ,  c
>.
Colors of variables: wff set class
Syntax hints:   wi 4   wa 97   wb 98   w3a 884  wal 1240   wceq 1242   wtru 1243  wex 1378   wcel 1390  weu 1897   _Vcvv 2551   [.wsbc 2758   <.cotp 3371
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 629  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-10 1393  ax-11 1394  ax-i12 1395  ax-bndl 1396  ax-4 1397  ax-14 1402  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019  ax-sep 3866  ax-pow 3918  ax-pr 3935
This theorem depends on definitions:  df-bi 110  df-3an 886  df-tru 1245  df-nf 1347  df-sb 1643  df-eu 1900  df-clab 2024  df-cleq 2030  df-clel 2033  df-nfc 2164  df-rex 2306  df-v 2553  df-sbc 2759  df-un 2916  df-in 2918  df-ss 2925  df-pw 3353  df-sn 3373  df-pr 3374  df-op 3376  df-ot 3377
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator