New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > eubii | GIF 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 | ⊢ (∃!xφ ↔ ∃!xψ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eubii.1 | . . . 4 ⊢ (φ ↔ ψ) | |
2 | 1 | a1i 10 | . . 3 ⊢ ( ⊤ → (φ ↔ ψ)) |
3 | 2 | eubidv 2212 | . 2 ⊢ ( ⊤ → (∃!xφ ↔ ∃!xψ)) |
4 | 3 | trud 1323 | 1 ⊢ (∃!xφ ↔ ∃!xψ) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 176 ⊤ wtru 1316 ∃!weu 2204 |
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-11 1746 |
This theorem depends on definitions: df-bi 177 df-tru 1319 df-ex 1542 df-nf 1545 df-eu 2208 |
This theorem is referenced by: cbveu 2224 2eu7 2290 2eu8 2291 reubiia 2796 cbvreu 2833 reuv 2874 euxfr2 3021 euxfr 3022 2reuswap 3038 2reu5lem1 3041 reuun2 3538 copsexg 4607 funeu2 5132 funcnv3 5157 fneu2 5188 tz6.12 5345 fsn 5432 |
Copyright terms: Public domain | W3C validator |