Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > eubii | GIF 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 2007 | . 2 ⊢ (⊤ → (∃!𝑥𝜑 ↔ ∃!𝑥𝜓)) |
4 | 3 | mptru 1340 | 1 ⊢ (∃!𝑥𝜑 ↔ ∃!𝑥𝜓) |
Colors of variables: wff set class |
Syntax hints: ↔ wb 104 ⊤wtru 1332 ∃!weu 1999 |
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 1423 ax-gen 1425 ax-ie1 1469 ax-ie2 1470 ax-4 1487 ax-17 1506 ax-ial 1514 |
This theorem depends on definitions: df-bi 116 df-tru 1334 df-nf 1437 df-eu 2002 |
This theorem is referenced by: cbveu 2023 2eu7 2093 reubiia 2615 cbvreu 2652 reuv 2705 euxfr2dc 2869 euxfrdc 2870 2reuswapdc 2888 reuun2 3359 zfnuleu 4052 copsexg 4166 funeu2 5149 funcnv3 5185 fneu2 5228 tz6.12 5449 f1ompt 5571 fsn 5592 climreu 11066 divalgb 11622 txcn 12444 |
Copyright terms: Public domain | W3C validator |