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 2399 with a disjoint variable condition, which does not require ax-13 2373. See cbvalvw 2044 for a version with two more disjoint variable conditions, requiring fewer axioms, and cbvalv 2401 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 232 | . . 3 ⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓)) |
5 | 1, 2, 4 | cbv3v 2337 | . 2 ⊢ (∀𝑥𝜑 → ∀𝑦𝜓) |
6 | 3 | biimprd 251 | . . . 4 ⊢ (𝑥 = 𝑦 → (𝜓 → 𝜑)) |
7 | 6 | equcoms 2028 | . . 3 ⊢ (𝑦 = 𝑥 → (𝜓 → 𝜑)) |
8 | 2, 1, 7 | cbv3v 2337 | . 2 ⊢ (∀𝑦𝜓 → ∀𝑥𝜑) |
9 | 5, 8 | impbii 212 | 1 ⊢ (∀𝑥𝜑 ↔ ∀𝑦𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 209 ∀wal 1541 Ⅎwnf 1791 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2016 ax-11 2160 ax-12 2177 |
This theorem depends on definitions: df-bi 210 df-an 400 df-ex 1788 df-nf 1792 |
This theorem is referenced by: cbvexv1 2344 cbval2v 2345 cbval2vOLD 2346 sb8v 2355 sbbib 2362 sbievg 2364 sb8eulem 2599 cbvmow 2604 abbi 2812 cleqh 2863 cleqf 2938 cbvralfw 3359 cbvralfwOLD 3360 cbvralf 3362 ralab2 3627 ralab2OLD 3628 cbvralcsf 3873 dfss2f 3907 ab0OLD 4307 elintab 4887 reusv2lem4 5311 cbviotaw 6366 cbviota 6369 sb8iota 6371 dffun6f 6415 findcard2 8868 findcard2OLD 8943 aceq1 9761 bnj1385 32556 sbcalf 36046 alrimii 36051 aomclem6 40635 rababg 40905 |
Copyright terms: Public domain | W3C validator |