![]() |
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 2397 with a disjoint variable condition, which does not require ax-13 2371. See cbvalvw 2040 for a version with two more disjoint variable conditions, requiring fewer axioms, and cbvalv 2399 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 228 | . . 3 ⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓)) |
5 | 1, 2, 4 | cbv3v 2332 | . 2 ⊢ (∀𝑥𝜑 → ∀𝑦𝜓) |
6 | 3 | biimprd 248 | . . . 4 ⊢ (𝑥 = 𝑦 → (𝜓 → 𝜑)) |
7 | 6 | equcoms 2024 | . . 3 ⊢ (𝑦 = 𝑥 → (𝜓 → 𝜑)) |
8 | 2, 1, 7 | cbv3v 2332 | . 2 ⊢ (∀𝑦𝜓 → ∀𝑥𝜑) |
9 | 5, 8 | impbii 208 | 1 ⊢ (∀𝑥𝜑 ↔ ∀𝑦𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∀wal 1540 Ⅎwnf 1786 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-11 2155 ax-12 2172 |
This theorem depends on definitions: df-bi 206 df-an 398 df-ex 1783 df-nf 1787 |
This theorem is referenced by: cbvexv1 2339 cbval2v 2340 sb8fOLD 2351 sbbib 2358 sbievg 2360 sb8eulem 2597 cbvmow 2602 abbi 2809 cleqh 2868 cleqf 2939 cbvralfw 3290 cbvralfwOLD 3307 cbvralf 3336 ralab2 3660 cbvralcsf 3905 dfss2f 3939 ab0OLD 4340 elintabOLD 4925 reusv2lem4 5361 cbviotaw 6460 cbviota 6463 sb8iota 6465 dffun6f 6519 findcard2 9115 findcard2OLD 9235 aceq1 10060 bnj1385 33484 sbcalf 36602 alrimii 36607 aomclem6 41415 rababg 41920 |
Copyright terms: Public domain | W3C validator |