![]() |
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 3358 with a disjoint variable condition, which does not require ax-10 2139, ax-13 2375. For a version not dependent on ax-11 2155 and ax-12, see cbvralvw 3235. (Contributed by NM, 7-Mar-2004.) Avoid ax-10 2139, ax-13 2375. (Revised by GG, 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 2895 | . . . 4 ⊢ Ⅎ𝑦 𝑥 ∈ 𝐴 |
3 | cbvralfw.3 | . . . 4 ⊢ Ⅎ𝑦𝜑 | |
4 | 2, 3 | nfim 1894 | . . 3 ⊢ Ⅎ𝑦(𝑥 ∈ 𝐴 → 𝜑) |
5 | cbvralfw.1 | . . . . 5 ⊢ Ⅎ𝑥𝐴 | |
6 | 5 | nfcri 2895 | . . . 4 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐴 |
7 | cbvralfw.4 | . . . 4 ⊢ Ⅎ𝑥𝜓 | |
8 | 6, 7 | nfim 1894 | . . 3 ⊢ Ⅎ𝑥(𝑦 ∈ 𝐴 → 𝜓) |
9 | eleq1w 2822 | . . . 4 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴)) | |
10 | cbvralfw.5 | . . . 4 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) | |
11 | 9, 10 | imbi12d 344 | . . 3 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐴 → 𝜑) ↔ (𝑦 ∈ 𝐴 → 𝜓))) |
12 | 4, 8, 11 | cbvalv1 2342 | . 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝜑) ↔ ∀𝑦(𝑦 ∈ 𝐴 → 𝜓)) |
13 | df-ral 3060 | . 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑)) | |
14 | df-ral 3060 | . 2 ⊢ (∀𝑦 ∈ 𝐴 𝜓 ↔ ∀𝑦(𝑦 ∈ 𝐴 → 𝜓)) | |
15 | 12, 13, 14 | 3bitr4i 303 | 1 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦 ∈ 𝐴 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 206 ∀wal 1535 Ⅎwnf 1780 ∈ wcel 2106 Ⅎwnfc 2888 ∀wral 3059 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1908 ax-6 1965 ax-7 2005 ax-8 2108 ax-11 2155 ax-12 2175 |
This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1777 df-nf 1781 df-clel 2814 df-nfc 2890 df-ral 3060 |
This theorem is referenced by: cbvrexfw 3303 cbvralw 3304 reusv2lem4 5407 reusv2 5409 ffnfvf 7140 nnwof 12954 nnindf 32826 scottexf 38155 scott0f 38156 evth2f 44953 evthf 44965 fmptff 45215 supxrleubrnmptf 45401 stoweidlem14 45970 stoweidlem28 45984 stoweidlem59 46015 |
Copyright terms: Public domain | W3C validator |