Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > eubii | Structured version Visualization version 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.) Avoid ax-5 1918. (Revised by Wolf Lammen, 27-Sep-2023.) |
Ref | Expression |
---|---|
eubii.1 | ⊢ (𝜑 ↔ 𝜓) |
Ref | Expression |
---|---|
eubii | ⊢ (∃!𝑥𝜑 ↔ ∃!𝑥𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eubii.1 | . . . 4 ⊢ (𝜑 ↔ 𝜓) | |
2 | 1 | exbii 1855 | . . 3 ⊢ (∃𝑥𝜑 ↔ ∃𝑥𝜓) |
3 | 1 | mobii 2547 | . . 3 ⊢ (∃*𝑥𝜑 ↔ ∃*𝑥𝜓) |
4 | 2, 3 | anbi12i 630 | . 2 ⊢ ((∃𝑥𝜑 ∧ ∃*𝑥𝜑) ↔ (∃𝑥𝜓 ∧ ∃*𝑥𝜓)) |
5 | df-eu 2568 | . 2 ⊢ (∃!𝑥𝜑 ↔ (∃𝑥𝜑 ∧ ∃*𝑥𝜑)) | |
6 | df-eu 2568 | . 2 ⊢ (∃!𝑥𝜓 ↔ (∃𝑥𝜓 ∧ ∃*𝑥𝜓)) | |
7 | 4, 5, 6 | 3bitr4i 306 | 1 ⊢ (∃!𝑥𝜑 ↔ ∃!𝑥𝜓) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 209 ∧ wa 399 ∃wex 1787 ∃*wmo 2537 ∃!weu 2567 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 |
This theorem depends on definitions: df-bi 210 df-an 400 df-ex 1788 df-mo 2539 df-eu 2568 |
This theorem is referenced by: cbveuwOLD 2607 cbveu 2608 2eu7 2658 2eu8 2659 exists1 2661 reuanid 3246 reubiia 3302 cbvreuw 3351 cbvreu 3356 reuv 3434 euxfr2w 3633 euxfrw 3634 euxfr2 3635 euxfr 3636 2reuswap 3659 2reuswap2 3660 2reu5lem1 3668 reuun2 4229 euelss 4236 reusv2lem4 5294 copsexgw 5373 copsexg 5374 funeu2 6406 funcnv3 6450 fneu2 6489 tz6.12 6740 f1ompt 6928 fsn 6950 oeeu 8331 dfac5lem1 9737 dfac5lem5 9741 zmin 12540 climreu 15117 divalglem10 15963 divalgb 15965 dfinito2 17509 dftermo2 17510 txcn 22523 nbusgredgeu0 27456 adjeu 29970 reuxfrdf 30558 bnj130 32567 bnj207 32574 bnj864 32615 reurab 33389 bj-nuliota 34965 poimirlem25 35539 poimirlem27 35541 aiotaval 44259 afveu 44317 tz6.12-1-afv 44338 tz6.12-afv2 44404 tz6.12-1-afv2 44405 pairreueq 44635 reutru 45824 |
Copyright terms: Public domain | W3C validator |