New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > eueq3 | Unicode version |
Description: Equality has existential uniqueness (split into 3 cases). (Contributed by NM, 5-Apr-1995.) (Proof shortened by Mario Carneiro, 28-Sep-2015.) |
Ref | Expression |
---|---|
eueq3.1 | |
eueq3.2 | |
eueq3.3 | |
eueq3.4 |
Ref | Expression |
---|---|
eueq3 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eueq3.1 | . . . 4 | |
2 | 1 | eueq1 3009 | . . 3 |
3 | ibar 490 | . . . . . 6 | |
4 | pm2.45 386 | . . . . . . . . . 10 | |
5 | eueq3.4 | . . . . . . . . . . . 12 | |
6 | 5 | imnani 412 | . . . . . . . . . . 11 |
7 | 6 | con2i 112 | . . . . . . . . . 10 |
8 | 4, 7 | jaoi 368 | . . . . . . . . 9 |
9 | 8 | con2i 112 | . . . . . . . 8 |
10 | 4 | con2i 112 | . . . . . . . . . 10 |
11 | 10 | bianfd 892 | . . . . . . . . 9 |
12 | 6 | bianfd 892 | . . . . . . . . 9 |
13 | 11, 12 | orbi12d 690 | . . . . . . . 8 |
14 | 9, 13 | mtbid 291 | . . . . . . 7 |
15 | biorf 394 | . . . . . . 7 | |
16 | 14, 15 | syl 15 | . . . . . 6 |
17 | 3, 16 | bitrd 244 | . . . . 5 |
18 | 3orrot 940 | . . . . . 6 | |
19 | df-3or 935 | . . . . . 6 | |
20 | 18, 19 | bitri 240 | . . . . 5 |
21 | 17, 20 | syl6bbr 254 | . . . 4 |
22 | 21 | eubidv 2212 | . . 3 |
23 | 2, 22 | mpbii 202 | . 2 |
24 | eueq3.3 | . . . 4 | |
25 | 24 | eueq1 3009 | . . 3 |
26 | ibar 490 | . . . . . 6 | |
27 | 6 | adantr 451 | . . . . . . . . 9 |
28 | pm2.46 387 | . . . . . . . . . 10 | |
29 | 28 | adantr 451 | . . . . . . . . 9 |
30 | 27, 29 | jaoi 368 | . . . . . . . 8 |
31 | 30 | con2i 112 | . . . . . . 7 |
32 | biorf 394 | . . . . . . 7 | |
33 | 31, 32 | syl 15 | . . . . . 6 |
34 | 26, 33 | bitrd 244 | . . . . 5 |
35 | df-3or 935 | . . . . 5 | |
36 | 34, 35 | syl6bbr 254 | . . . 4 |
37 | 36 | eubidv 2212 | . . 3 |
38 | 25, 37 | mpbii 202 | . 2 |
39 | eueq3.2 | . . . 4 | |
40 | 39 | eueq1 3009 | . . 3 |
41 | ibar 490 | . . . . . 6 | |
42 | simpl 443 | . . . . . . . . 9 | |
43 | simpl 443 | . . . . . . . . 9 | |
44 | 42, 43 | orim12i 502 | . . . . . . . 8 |
45 | 44 | con3i 127 | . . . . . . 7 |
46 | biorf 394 | . . . . . . 7 | |
47 | 45, 46 | syl 15 | . . . . . 6 |
48 | 41, 47 | bitrd 244 | . . . . 5 |
49 | 3orcomb 944 | . . . . . 6 | |
50 | df-3or 935 | . . . . . 6 | |
51 | 49, 50 | bitri 240 | . . . . 5 |
52 | 48, 51 | syl6bbr 254 | . . . 4 |
53 | 52 | eubidv 2212 | . . 3 |
54 | 40, 53 | mpbii 202 | . 2 |
55 | 23, 38, 54 | ecase3 907 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wn 3 wb 176 wo 357 wa 358 w3o 933 wceq 1642 wcel 1710 weu 2204 cvv 2859 |
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 ax-ext 2334 |
This theorem depends on definitions: df-bi 177 df-or 359 df-an 360 df-3or 935 df-tru 1319 df-ex 1542 df-nf 1545 df-sb 1649 df-eu 2208 df-mo 2209 df-clab 2340 df-cleq 2346 df-clel 2349 df-v 2861 |
This theorem is referenced by: moeq3 3013 |
Copyright terms: Public domain | W3C validator |