Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > cbvralfw | Structured version Visualization version GIF version |
Description: Rule used to change bound variables, using implicit substitution. Version of cbvralf 3361 with a disjoint variable condition, which does not require ax-10 2139, ax-13 2372. (Contributed by NM, 7-Mar-2004.) (Revised by Gino Giotto, 23-May-2024.) |
Ref | Expression |
---|---|
cbvralfw.1 | ⊢ Ⅎ𝑥𝐴 |
cbvralfw.2 | ⊢ Ⅎ𝑦𝐴 |
cbvralfw.3 | ⊢ Ⅎ𝑦𝜑 |
cbvralfw.4 | ⊢ Ⅎ𝑥𝜓 |
cbvralfw.5 | ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) |
Ref | Expression |
---|---|
cbvralfw | ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦 ∈ 𝐴 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cbvralfw.2 | . . . . 5 ⊢ Ⅎ𝑦𝐴 | |
2 | 1 | nfcri 2893 | . . . 4 ⊢ Ⅎ𝑦 𝑥 ∈ 𝐴 |
3 | cbvralfw.3 | . . . 4 ⊢ Ⅎ𝑦𝜑 | |
4 | 2, 3 | nfim 1900 | . . 3 ⊢ Ⅎ𝑦(𝑥 ∈ 𝐴 → 𝜑) |
5 | cbvralfw.1 | . . . . 5 ⊢ Ⅎ𝑥𝐴 | |
6 | 5 | nfcri 2893 | . . . 4 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐴 |
7 | cbvralfw.4 | . . . 4 ⊢ Ⅎ𝑥𝜓 | |
8 | 6, 7 | nfim 1900 | . . 3 ⊢ Ⅎ𝑥(𝑦 ∈ 𝐴 → 𝜓) |
9 | eleq1w 2821 | . . . 4 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴)) | |
10 | cbvralfw.5 | . . . 4 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) | |
11 | 9, 10 | imbi12d 344 | . . 3 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐴 → 𝜑) ↔ (𝑦 ∈ 𝐴 → 𝜓))) |
12 | 4, 8, 11 | cbvalv1 2340 | . 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝜑) ↔ ∀𝑦(𝑦 ∈ 𝐴 → 𝜓)) |
13 | df-ral 3068 | . 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑)) | |
14 | df-ral 3068 | . 2 ⊢ (∀𝑦 ∈ 𝐴 𝜓 ↔ ∀𝑦(𝑦 ∈ 𝐴 → 𝜓)) | |
15 | 12, 13, 14 | 3bitr4i 302 | 1 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦 ∈ 𝐴 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∀wal 1537 Ⅎwnf 1787 ∈ wcel 2108 Ⅎwnfc 2886 ∀wral 3063 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1799 ax-4 1813 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2110 ax-11 2156 ax-12 2173 |
This theorem depends on definitions: df-bi 206 df-an 396 df-ex 1784 df-nf 1788 df-clel 2817 df-nfc 2888 df-ral 3068 |
This theorem is referenced by: cbvrexfw 3360 cbvralw 3363 reusv2lem4 5319 reusv2 5321 ffnfvf 6975 nnwof 12583 nnindf 31035 scottexf 36253 scott0f 36254 evth2f 42447 evthf 42459 supxrleubrnmptf 42881 stoweidlem14 43445 stoweidlem28 43459 stoweidlem59 43490 |
Copyright terms: Public domain | W3C validator |