![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > reu8nf | Structured version Visualization version GIF version |
Description: Restricted uniqueness using implicit substitution. This version of reu8 3730 uses a nonfreeness hypothesis for 𝑥 and 𝜓 instead of distinct variable conditions. (Contributed by AV, 21-Jan-2022.) |
Ref | Expression |
---|---|
reu8nf.1 | ⊢ Ⅎ𝑥𝜓 |
reu8nf.2 | ⊢ Ⅎ𝑥𝜒 |
reu8nf.3 | ⊢ (𝑥 = 𝑤 → (𝜑 ↔ 𝜒)) |
reu8nf.4 | ⊢ (𝑤 = 𝑦 → (𝜒 ↔ 𝜓)) |
Ref | Expression |
---|---|
reu8nf | ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐴 (𝜑 ∧ ∀𝑦 ∈ 𝐴 (𝜓 → 𝑥 = 𝑦))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfv 1915 | . . 3 ⊢ Ⅎ𝑤𝜑 | |
2 | reu8nf.2 | . . 3 ⊢ Ⅎ𝑥𝜒 | |
3 | reu8nf.3 | . . 3 ⊢ (𝑥 = 𝑤 → (𝜑 ↔ 𝜒)) | |
4 | 1, 2, 3 | cbvreuw 3404 | . 2 ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑤 ∈ 𝐴 𝜒) |
5 | reu8nf.4 | . . 3 ⊢ (𝑤 = 𝑦 → (𝜒 ↔ 𝜓)) | |
6 | 5 | reu8 3730 | . 2 ⊢ (∃!𝑤 ∈ 𝐴 𝜒 ↔ ∃𝑤 ∈ 𝐴 (𝜒 ∧ ∀𝑦 ∈ 𝐴 (𝜓 → 𝑤 = 𝑦))) |
7 | nfcv 2901 | . . . . 5 ⊢ Ⅎ𝑥𝐴 | |
8 | reu8nf.1 | . . . . . 6 ⊢ Ⅎ𝑥𝜓 | |
9 | nfv 1915 | . . . . . 6 ⊢ Ⅎ𝑥 𝑤 = 𝑦 | |
10 | 8, 9 | nfim 1897 | . . . . 5 ⊢ Ⅎ𝑥(𝜓 → 𝑤 = 𝑦) |
11 | 7, 10 | nfralw 3306 | . . . 4 ⊢ Ⅎ𝑥∀𝑦 ∈ 𝐴 (𝜓 → 𝑤 = 𝑦) |
12 | 2, 11 | nfan 1900 | . . 3 ⊢ Ⅎ𝑥(𝜒 ∧ ∀𝑦 ∈ 𝐴 (𝜓 → 𝑤 = 𝑦)) |
13 | nfv 1915 | . . 3 ⊢ Ⅎ𝑤(𝜑 ∧ ∀𝑦 ∈ 𝐴 (𝜓 → 𝑥 = 𝑦)) | |
14 | 3 | bicomd 222 | . . . . 5 ⊢ (𝑥 = 𝑤 → (𝜒 ↔ 𝜑)) |
15 | 14 | equcoms 2021 | . . . 4 ⊢ (𝑤 = 𝑥 → (𝜒 ↔ 𝜑)) |
16 | equequ1 2026 | . . . . . 6 ⊢ (𝑤 = 𝑥 → (𝑤 = 𝑦 ↔ 𝑥 = 𝑦)) | |
17 | 16 | imbi2d 339 | . . . . 5 ⊢ (𝑤 = 𝑥 → ((𝜓 → 𝑤 = 𝑦) ↔ (𝜓 → 𝑥 = 𝑦))) |
18 | 17 | ralbidv 3175 | . . . 4 ⊢ (𝑤 = 𝑥 → (∀𝑦 ∈ 𝐴 (𝜓 → 𝑤 = 𝑦) ↔ ∀𝑦 ∈ 𝐴 (𝜓 → 𝑥 = 𝑦))) |
19 | 15, 18 | anbi12d 629 | . . 3 ⊢ (𝑤 = 𝑥 → ((𝜒 ∧ ∀𝑦 ∈ 𝐴 (𝜓 → 𝑤 = 𝑦)) ↔ (𝜑 ∧ ∀𝑦 ∈ 𝐴 (𝜓 → 𝑥 = 𝑦)))) |
20 | 12, 13, 19 | cbvrexw 3302 | . 2 ⊢ (∃𝑤 ∈ 𝐴 (𝜒 ∧ ∀𝑦 ∈ 𝐴 (𝜓 → 𝑤 = 𝑦)) ↔ ∃𝑥 ∈ 𝐴 (𝜑 ∧ ∀𝑦 ∈ 𝐴 (𝜓 → 𝑥 = 𝑦))) |
21 | 4, 6, 20 | 3bitri 296 | 1 ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐴 (𝜑 ∧ ∀𝑦 ∈ 𝐴 (𝜓 → 𝑥 = 𝑦))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ wa 394 Ⅎwnf 1783 ∀wral 3059 ∃wrex 3068 ∃!wreu 3372 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1911 ax-6 1969 ax-7 2009 ax-8 2106 ax-10 2135 ax-11 2152 ax-12 2169 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 844 df-tru 1542 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2532 df-eu 2561 df-clel 2808 df-nfc 2883 df-ral 3060 df-rex 3069 df-rmo 3374 df-reu 3375 |
This theorem is referenced by: reusngf 4677 reuprg0 4707 reuop 6293 reuccatpfxs1 14703 reupr 46490 |
Copyright terms: Public domain | W3C validator |