| 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 1910. (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 1848 | . . 3 ⊢ (∃𝑥𝜑 ↔ ∃𝑥𝜓) |
| 3 | 1 | mobii 2548 | . . 3 ⊢ (∃*𝑥𝜑 ↔ ∃*𝑥𝜓) |
| 4 | 2, 3 | anbi12i 628 | . 2 ⊢ ((∃𝑥𝜑 ∧ ∃*𝑥𝜑) ↔ (∃𝑥𝜓 ∧ ∃*𝑥𝜓)) |
| 5 | df-eu 2569 | . 2 ⊢ (∃!𝑥𝜑 ↔ (∃𝑥𝜑 ∧ ∃*𝑥𝜑)) | |
| 6 | df-eu 2569 | . 2 ⊢ (∃!𝑥𝜓 ↔ (∃𝑥𝜓 ∧ ∃*𝑥𝜓)) | |
| 7 | 4, 5, 6 | 3bitr4i 303 | 1 ⊢ (∃!𝑥𝜑 ↔ ∃!𝑥𝜓) |
| Colors of variables: wff setvar class |
| Syntax hints: ↔ wb 206 ∧ wa 395 ∃wex 1779 ∃*wmo 2538 ∃!weu 2568 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1780 df-mo 2540 df-eu 2569 |
| This theorem is referenced by: cbveu 2607 2eu7 2658 2eu8 2659 exists1 2661 reubiia 3387 reuanidOLD 3393 cbvreuwOLD 3415 cbvreu 3428 reuv 3510 reurab 3707 euxfr2w 3726 euxfrw 3727 euxfr2 3728 euxfr 3729 2reuswap 3752 2reuswap2 3753 2reu5lem1 3761 reuun2 4325 euelss 4332 reusv2lem4 5401 copsexgw 5495 copsexg 5496 funeu2 6592 funcnv3 6636 fneu2 6679 tz6.12 6931 f1ompt 7131 fsn 7155 oeeu 8641 dfac5lem1 10163 dfac5lem5 10167 zmin 12986 climreu 15592 divalglem10 16439 divalgb 16441 dfinito2 18048 dftermo2 18049 txcn 23634 nbusgredgeu0 29385 adjeu 31908 reuxfrdf 32510 bnj130 34888 bnj207 34895 bnj864 34936 reueqi 36190 reueqbii 36191 bj-nuliota 37058 poimirlem25 37652 poimirlem27 37654 tfsconcatlem 43349 dfac5prim 45007 modelac8prim 45009 aiotaval 47107 afveu 47165 tz6.12-1-afv 47186 tz6.12-afv2 47252 tz6.12-1-afv2 47253 pairreueq 47497 reutru 48724 |
| Copyright terms: Public domain | W3C validator |