![]() |
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 3354 with a disjoint variable condition, which does not require ax-10 2135, ax-13 2369. For a version not dependent on ax-11 2152 and ax-12, see cbvralvw 3232. (Contributed by NM, 7-Mar-2004.) Avoid ax-10 2135, ax-13 2369. (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 2888 | . . . 4 ⊢ Ⅎ𝑦 𝑥 ∈ 𝐴 |
3 | cbvralfw.3 | . . . 4 ⊢ Ⅎ𝑦𝜑 | |
4 | 2, 3 | nfim 1897 | . . 3 ⊢ Ⅎ𝑦(𝑥 ∈ 𝐴 → 𝜑) |
5 | cbvralfw.1 | . . . . 5 ⊢ Ⅎ𝑥𝐴 | |
6 | 5 | nfcri 2888 | . . . 4 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐴 |
7 | cbvralfw.4 | . . . 4 ⊢ Ⅎ𝑥𝜓 | |
8 | 6, 7 | nfim 1897 | . . 3 ⊢ Ⅎ𝑥(𝑦 ∈ 𝐴 → 𝜓) |
9 | eleq1w 2814 | . . . 4 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴)) | |
10 | cbvralfw.5 | . . . 4 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) | |
11 | 9, 10 | imbi12d 343 | . . 3 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐴 → 𝜑) ↔ (𝑦 ∈ 𝐴 → 𝜓))) |
12 | 4, 8, 11 | cbvalv1 2335 | . 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝜑) ↔ ∀𝑦(𝑦 ∈ 𝐴 → 𝜓)) |
13 | df-ral 3060 | . 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑)) | |
14 | df-ral 3060 | . 2 ⊢ (∀𝑦 ∈ 𝐴 𝜓 ↔ ∀𝑦(𝑦 ∈ 𝐴 → 𝜓)) | |
15 | 12, 13, 14 | 3bitr4i 302 | 1 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦 ∈ 𝐴 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∀wal 1537 Ⅎwnf 1783 ∈ wcel 2104 Ⅎwnfc 2881 ∀wral 3059 |
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-11 2152 ax-12 2169 |
This theorem depends on definitions: df-bi 206 df-an 395 df-ex 1780 df-nf 1784 df-clel 2808 df-nfc 2883 df-ral 3060 |
This theorem is referenced by: cbvrexfw 3300 cbvralw 3301 reusv2lem4 5398 reusv2 5400 ffnfvf 7120 nnwof 12902 nnindf 32292 scottexf 37339 scott0f 37340 evth2f 44001 evthf 44013 fmptff 44272 supxrleubrnmptf 44459 stoweidlem14 45028 stoweidlem28 45042 stoweidlem59 45073 |
Copyright terms: Public domain | W3C validator |