| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > cbvalv1 | Structured version Visualization version GIF version | ||
| Description: Rule used to change bound variables, using implicit substitution. Version of cbval 2403 with a disjoint variable condition, which does not require ax-13 2377. See cbvalvw 2035 for a version with two more disjoint variable conditions, requiring fewer axioms, and cbvalv 2405 for another variant. (Contributed by NM, 13-May-1993.) (Revised by BJ, 31-May-2019.) |
| Ref | Expression |
|---|---|
| cbvalv1.nf1 | ⊢ Ⅎ𝑦𝜑 |
| cbvalv1.nf2 | ⊢ Ⅎ𝑥𝜓 |
| cbvalv1.1 | ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) |
| Ref | Expression |
|---|---|
| cbvalv1 | ⊢ (∀𝑥𝜑 ↔ ∀𝑦𝜓) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | cbvalv1.nf1 | . . 3 ⊢ Ⅎ𝑦𝜑 | |
| 2 | cbvalv1.nf2 | . . 3 ⊢ Ⅎ𝑥𝜓 | |
| 3 | cbvalv1.1 | . . . 4 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) | |
| 4 | 3 | biimpd 229 | . . 3 ⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓)) |
| 5 | 1, 2, 4 | cbv3v 2337 | . 2 ⊢ (∀𝑥𝜑 → ∀𝑦𝜓) |
| 6 | 3 | biimprd 248 | . . . 4 ⊢ (𝑥 = 𝑦 → (𝜓 → 𝜑)) |
| 7 | 6 | equcoms 2019 | . . 3 ⊢ (𝑦 = 𝑥 → (𝜓 → 𝜑)) |
| 8 | 2, 1, 7 | cbv3v 2337 | . 2 ⊢ (∀𝑦𝜓 → ∀𝑥𝜑) |
| 9 | 5, 8 | impbii 209 | 1 ⊢ (∀𝑥𝜑 ↔ ∀𝑦𝜓) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 206 ∀wal 1538 Ⅎwnf 1783 |
| 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-11 2157 ax-12 2177 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1780 df-nf 1784 |
| This theorem is referenced by: cbvexv1 2344 cbval2v 2345 sb8fOLD 2357 sbbib 2364 cbvsbvf 2366 sb8eulem 2598 cbvmow 2603 abbib 2811 cleqh 2871 cleqf 2934 cbvralfw 3304 cbvralf 3360 ralab2 3703 cbvralcsf 3941 dfssf 3974 elintabOLD 4959 reusv2lem4 5401 cbviotaw 6521 cbviota 6523 sb8iota 6525 dffun6f 6579 findcard2 9204 aceq1 10157 bnj1385 34846 sbcalf 38121 alrimii 38126 aomclem6 43071 rababg 43587 |
| Copyright terms: Public domain | W3C validator |