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

Theorem eueq3dc 2709
Description: Equality has existential uniqueness (split into 3 cases). (Contributed by NM, 5-Apr-1995.) (Proof shortened by Mario Carneiro, 28-Sep-2015.)
Hypotheses
Ref Expression
eueq3dc.1  _V
eueq3dc.2  _V
eueq3dc.3  C 
_V
eueq3dc.4
Assertion
Ref Expression
eueq3dc DECID DECID  C
Distinct variable groups:   ,   ,   ,   ,   , C

Proof of Theorem eueq3dc
StepHypRef Expression
1 dcor 842 . 2 DECID DECID DECID
2 df-dc 742 . . 3 DECID
3 eueq3dc.1 . . . . . . 7  _V
43eueq1 2707 . . . . . 6
5 ibar 285 . . . . . . . . 9
6 pm2.45 656 . . . . . . . . . . . . 13
7 eueq3dc.4 . . . . . . . . . . . . . . 15
87imnani 624 . . . . . . . . . . . . . 14
98con2i 557 . . . . . . . . . . . . 13
106, 9jaoi 635 . . . . . . . . . . . 12
1110con2i 557 . . . . . . . . . . 11
126con2i 557 . . . . . . . . . . . . 13
1312bianfd 854 . . . . . . . . . . . 12
148bianfd 854 . . . . . . . . . . . 12  C
1513, 14orbi12d 706 . . . . . . . . . . 11  C
1611, 15mtbid 596 . . . . . . . . . 10  C
17 biorf 662 . . . . . . . . . 10  C  C
1816, 17syl 14 . . . . . . . . 9  C
195, 18bitrd 177 . . . . . . . 8  C
20 3orrot 890 . . . . . . . . 9  C  C
21 df-3or 885 . . . . . . . . 9  C  C
2220, 21bitri 173 . . . . . . . 8  C  C
2319, 22syl6bbr 187 . . . . . . 7  C
2423eubidv 1905 . . . . . 6  C
254, 24mpbii 136 . . . . 5  C
26 eueq3dc.3 . . . . . . 7  C 
_V
2726eueq1 2707 . . . . . 6  C
28 ibar 285 . . . . . . . . 9  C  C
298adantr 261 . . . . . . . . . . . 12
30 pm2.46 657 . . . . . . . . . . . . 13
3130adantr 261 . . . . . . . . . . . 12
3229, 31jaoi 635 . . . . . . . . . . 11
3332con2i 557 . . . . . . . . . 10
34 biorf 662 . . . . . . . . . 10  C  C
3533, 34syl 14 . . . . . . . . 9  C  C
3628, 35bitrd 177 . . . . . . . 8  C  C
37 df-3or 885 . . . . . . . 8  C  C
3836, 37syl6bbr 187 . . . . . . 7  C  C
3938eubidv 1905 . . . . . 6  C  C
4027, 39mpbii 136 . . . . 5  C
4125, 40jaoi 635 . . . 4  C
42 eueq3dc.2 . . . . . 6  _V
4342eueq1 2707 . . . . 5
44 ibar 285 . . . . . . . 8
45 simpl 102 . . . . . . . . . . 11
46 simpl 102 . . . . . . . . . . 11  C
4745, 46orim12i 675 . . . . . . . . . 10  C
4847con3i 561 . . . . . . . . 9  C
49 biorf 662 . . . . . . . . 9  C  C
5048, 49syl 14 . . . . . . . 8  C
5144, 50bitrd 177 . . . . . . 7  C
52 3orcomb 893 . . . . . . . 8  C  C
53 df-3or 885 . . . . . . . 8  C  C
5452, 53bitri 173 . . . . . . 7  C  C
5551, 54syl6bbr 187 . . . . . 6  C
5655eubidv 1905 . . . . 5  C
5743, 56mpbii 136 . . . 4  C
5841, 57jaoi 635 . . 3  C
592, 58sylbi 114 . 2 DECID  C
601, 59syl6 29 1 DECID DECID  C
Colors of variables: wff set class
Syntax hints:   wn 3   wi 4   wa 97   wb 98   wo 628  DECID wdc 741   w3o 883   wceq 1242   wcel 1390  weu 1897   _Vcvv 2551
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-in1 544  ax-in2 545  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-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019
This theorem depends on definitions:  df-bi 110  df-dc 742  df-3or 885  df-nf 1347  df-sb 1643  df-eu 1900  df-mo 1901  df-clab 2024  df-cleq 2030  df-clel 2033  df-v 2553
This theorem is referenced by:  moeq3dc  2711
  Copyright terms: Public domain W3C validator