| 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 3360 with a disjoint variable condition, which does not require ax-10 2141, ax-13 2377. For a version not dependent on ax-11 2157 and ax-12, see cbvralvw 3237. (Contributed by NM, 7-Mar-2004.) Avoid ax-10 2141, ax-13 2377. (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 2897 | . . . 4 ⊢ Ⅎ𝑦 𝑥 ∈ 𝐴 |
| 3 | cbvralfw.3 | . . . 4 ⊢ Ⅎ𝑦𝜑 | |
| 4 | 2, 3 | nfim 1896 | . . 3 ⊢ Ⅎ𝑦(𝑥 ∈ 𝐴 → 𝜑) |
| 5 | cbvralfw.1 | . . . . 5 ⊢ Ⅎ𝑥𝐴 | |
| 6 | 5 | nfcri 2897 | . . . 4 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐴 |
| 7 | cbvralfw.4 | . . . 4 ⊢ Ⅎ𝑥𝜓 | |
| 8 | 6, 7 | nfim 1896 | . . 3 ⊢ Ⅎ𝑥(𝑦 ∈ 𝐴 → 𝜓) |
| 9 | eleq1w 2824 | . . . 4 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴)) | |
| 10 | cbvralfw.5 | . . . 4 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) | |
| 11 | 9, 10 | imbi12d 344 | . . 3 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐴 → 𝜑) ↔ (𝑦 ∈ 𝐴 → 𝜓))) |
| 12 | 4, 8, 11 | cbvalv1 2343 | . 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝜑) ↔ ∀𝑦(𝑦 ∈ 𝐴 → 𝜓)) |
| 13 | df-ral 3062 | . 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑)) | |
| 14 | df-ral 3062 | . 2 ⊢ (∀𝑦 ∈ 𝐴 𝜓 ↔ ∀𝑦(𝑦 ∈ 𝐴 → 𝜓)) | |
| 15 | 12, 13, 14 | 3bitr4i 303 | 1 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦 ∈ 𝐴 𝜓) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 206 ∀wal 1538 Ⅎwnf 1783 ∈ wcel 2108 Ⅎwnfc 2890 ∀wral 3061 |
| 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 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-11 2157 ax-12 2177 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1780 df-nf 1784 df-clel 2816 df-nfc 2892 df-ral 3062 |
| This theorem is referenced by: cbvrexfw 3305 cbvralw 3306 reusv2lem4 5401 reusv2 5403 ffnfvf 7140 nnwof 12956 nnindf 32821 scottexf 38175 scott0f 38176 evth2f 45020 evthf 45032 fmptff 45276 supxrleubrnmptf 45462 stoweidlem14 46029 stoweidlem28 46043 stoweidlem59 46074 |
| Copyright terms: Public domain | W3C validator |