![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > eubii | Unicode version |
Description: Introduce uniqueness quantifier to both sides of an equivalence. (Contributed by NM, 9-Jul-1994.) (Revised by Mario Carneiro, 6-Oct-2016.) |
Ref | Expression |
---|---|
eubii.1 |
![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
eubii |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eubii.1 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | a1i 9 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | 2 | eubidv 1908 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 3 | trud 1252 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() |
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-5 1336 ax-gen 1338 ax-ie1 1382 ax-ie2 1383 ax-4 1400 ax-17 1419 ax-ial 1427 |
This theorem depends on definitions: df-bi 110 df-tru 1246 df-nf 1350 df-eu 1903 |
This theorem is referenced by: cbveu 1924 2eu7 1994 reubiia 2494 cbvreu 2531 reuv 2573 euxfr2dc 2726 euxfrdc 2727 2reuswapdc 2743 reuun2 3220 zfnuleu 3881 copsexg 3981 funeu2 4927 funcnv3 4961 fneu2 5004 tz6.12 5201 f1ompt 5320 fsn 5335 climreu 9818 |
Copyright terms: Public domain | W3C validator |