Mathbox for Alexander van der Vekens |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > Mathboxes > 2reu4a | Structured version Visualization version Unicode version |
Description: Definition of double restricted existential uniqueness ("exactly one and exactly one "), analogous to 2eu4 2556 with the additional requirement that the restricting classes are not empty (which is not necessary as shown in 2reu4 41190). (Contributed by Alexander van der Vekens, 1-Jul-2017.) |
Ref | Expression |
---|---|
2reu4a |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | reu3 3396 | . . . 4 | |
2 | reu3 3396 | . . . 4 | |
3 | 1, 2 | anbi12i 733 | . . 3 |
4 | 3 | a1i 11 | . 2 |
5 | an4 865 | . . 3 | |
6 | 5 | a1i 11 | . 2 |
7 | rexcom 3099 | . . . . . 6 | |
8 | 7 | anbi2i 730 | . . . . 5 |
9 | anidm 676 | . . . . 5 | |
10 | 8, 9 | bitri 264 | . . . 4 |
11 | 10 | a1i 11 | . . 3 |
12 | r19.26 3064 | . . . . . . . 8 | |
13 | nfra1 2941 | . . . . . . . . . . . . . 14 | |
14 | 13 | r19.3rz 4062 | . . . . . . . . . . . . 13 |
15 | 14 | bicomd 213 | . . . . . . . . . . . 12 |
16 | 15 | adantr 481 | . . . . . . . . . . 11 |
17 | 16 | adantr 481 | . . . . . . . . . 10 |
18 | 17 | anbi2d 740 | . . . . . . . . 9 |
19 | jcab 907 | . . . . . . . . . . . . . 14 | |
20 | 19 | ralbii 2980 | . . . . . . . . . . . . 13 |
21 | r19.26 3064 | . . . . . . . . . . . . 13 | |
22 | 20, 21 | bitri 264 | . . . . . . . . . . . 12 |
23 | 22 | ralbii 2980 | . . . . . . . . . . 11 |
24 | r19.26 3064 | . . . . . . . . . . 11 | |
25 | 23, 24 | bitri 264 | . . . . . . . . . 10 |
26 | 25 | a1i 11 | . . . . . . . . 9 |
27 | 18, 26 | bitr4d 271 | . . . . . . . 8 |
28 | 12, 27 | syl5rbb 273 | . . . . . . 7 |
29 | r19.26 3064 | . . . . . . . . 9 | |
30 | nfra1 2941 | . . . . . . . . . . . . 13 | |
31 | 30 | r19.3rz 4062 | . . . . . . . . . . . 12 |
32 | 31 | ad2antlr 763 | . . . . . . . . . . 11 |
33 | 32 | bicomd 213 | . . . . . . . . . 10 |
34 | ralcom 3098 | . . . . . . . . . . 11 | |
35 | 34 | a1i 11 | . . . . . . . . . 10 |
36 | 33, 35 | anbi12d 747 | . . . . . . . . 9 |
37 | 29, 36 | syl5bb 272 | . . . . . . . 8 |
38 | 37 | ralbidv 2986 | . . . . . . 7 |
39 | 28, 38 | bitr4d 271 | . . . . . 6 |
40 | r19.23v 3023 | . . . . . . . . 9 | |
41 | r19.23v 3023 | . . . . . . . . 9 | |
42 | 40, 41 | anbi12i 733 | . . . . . . . 8 |
43 | 42 | 2ralbii 2981 | . . . . . . 7 |
44 | 43 | a1i 11 | . . . . . 6 |
45 | neneq 2800 | . . . . . . . . . . 11 | |
46 | neneq 2800 | . . . . . . . . . . 11 | |
47 | 45, 46 | anim12i 590 | . . . . . . . . . 10 |
48 | 47 | olcd 408 | . . . . . . . . 9 |
49 | dfbi3 994 | . . . . . . . . 9 | |
50 | 48, 49 | sylibr 224 | . . . . . . . 8 |
51 | nfre1 3005 | . . . . . . . . . 10 | |
52 | nfv 1843 | . . . . . . . . . 10 | |
53 | 51, 52 | nfim 1825 | . . . . . . . . 9 |
54 | nfre1 3005 | . . . . . . . . . 10 | |
55 | nfv 1843 | . . . . . . . . . 10 | |
56 | 54, 55 | nfim 1825 | . . . . . . . . 9 |
57 | 53, 56 | raaan2 41175 | . . . . . . . 8 |
58 | 50, 57 | syl 17 | . . . . . . 7 |
59 | 58 | adantr 481 | . . . . . 6 |
60 | 39, 44, 59 | 3bitrd 294 | . . . . 5 |
61 | 60 | 2rexbidva 3056 | . . . 4 |
62 | reeanv 3107 | . . . 4 | |
63 | 61, 62 | syl6rbb 277 | . . 3 |
64 | 11, 63 | anbi12d 747 | . 2 |
65 | 4, 6, 64 | 3bitrd 294 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wn 3 wi 4 wb 196 wo 383 wa 384 wceq 1483 wcel 1990 wne 2794 wral 2912 wrex 2913 wreu 2914 c0 3915 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 |
This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-mo 2475 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ne 2795 df-ral 2917 df-rex 2918 df-reu 2919 df-rmo 2920 df-v 3202 df-dif 3577 df-nul 3916 |
This theorem is referenced by: 2reu4 41190 |
Copyright terms: Public domain | W3C validator |