![]() |
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 3357 with a disjoint variable condition, which does not require ax-10 2138, ax-13 2372. For a version not dependent on ax-11 2155 and ax-12, see cbvralvw 3235. (Contributed by NM, 7-Mar-2004.) Avoid ax-10 2138, ax-13 2372. (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 2891 | . . . 4 ⊢ Ⅎ𝑦 𝑥 ∈ 𝐴 |
3 | cbvralfw.3 | . . . 4 ⊢ Ⅎ𝑦𝜑 | |
4 | 2, 3 | nfim 1900 | . . 3 ⊢ Ⅎ𝑦(𝑥 ∈ 𝐴 → 𝜑) |
5 | cbvralfw.1 | . . . . 5 ⊢ Ⅎ𝑥𝐴 | |
6 | 5 | nfcri 2891 | . . . 4 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐴 |
7 | cbvralfw.4 | . . . 4 ⊢ Ⅎ𝑥𝜓 | |
8 | 6, 7 | nfim 1900 | . . 3 ⊢ Ⅎ𝑥(𝑦 ∈ 𝐴 → 𝜓) |
9 | eleq1w 2817 | . . . 4 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴)) | |
10 | cbvralfw.5 | . . . 4 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) | |
11 | 9, 10 | imbi12d 345 | . . 3 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐴 → 𝜑) ↔ (𝑦 ∈ 𝐴 → 𝜓))) |
12 | 4, 8, 11 | cbvalv1 2338 | . 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝜑) ↔ ∀𝑦(𝑦 ∈ 𝐴 → 𝜓)) |
13 | df-ral 3063 | . 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑)) | |
14 | df-ral 3063 | . 2 ⊢ (∀𝑦 ∈ 𝐴 𝜓 ↔ ∀𝑦(𝑦 ∈ 𝐴 → 𝜓)) | |
15 | 12, 13, 14 | 3bitr4i 303 | 1 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦 ∈ 𝐴 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∀wal 1540 Ⅎwnf 1786 ∈ wcel 2107 Ⅎwnfc 2884 ∀wral 3062 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-11 2155 ax-12 2172 |
This theorem depends on definitions: df-bi 206 df-an 398 df-ex 1783 df-nf 1787 df-clel 2811 df-nfc 2886 df-ral 3063 |
This theorem is referenced by: cbvrexfw 3303 cbvralw 3304 reusv2lem4 5400 reusv2 5402 ffnfvf 7119 nnwof 12898 nnindf 32025 scottexf 37036 scott0f 37037 evth2f 43699 evthf 43711 fmptff 43974 supxrleubrnmptf 44161 stoweidlem14 44730 stoweidlem28 44744 stoweidlem59 44775 |
Copyright terms: Public domain | W3C validator |