Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > eubii | Unicode version |
Description: Introduce unique existential 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 1985 | . 2 |
4 | 3 | mptru 1325 | 1 |
Colors of variables: wff set class |
Syntax hints: wb 104 wtru 1317 weu 1977 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-5 1408 ax-gen 1410 ax-ie1 1454 ax-ie2 1455 ax-4 1472 ax-17 1491 ax-ial 1499 |
This theorem depends on definitions: df-bi 116 df-tru 1319 df-nf 1422 df-eu 1980 |
This theorem is referenced by: cbveu 2001 2eu7 2071 reubiia 2592 cbvreu 2629 reuv 2679 euxfr2dc 2842 euxfrdc 2843 2reuswapdc 2861 reuun2 3329 zfnuleu 4022 copsexg 4136 funeu2 5119 funcnv3 5155 fneu2 5198 tz6.12 5417 f1ompt 5539 fsn 5560 climreu 11034 divalgb 11549 txcn 12371 |
Copyright terms: Public domain | W3C validator |