![]() |
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 2391 with a disjoint variable condition, which does not require ax-13 2365. See cbvalvw 2031 for a version with two more disjoint variable conditions, requiring fewer axioms, and cbvalv 2393 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 2325 | . 2 ⊢ (∀𝑥𝜑 → ∀𝑦𝜓) |
6 | 3 | biimprd 247 | . . . 4 ⊢ (𝑥 = 𝑦 → (𝜓 → 𝜑)) |
7 | 6 | equcoms 2015 | . . 3 ⊢ (𝑦 = 𝑥 → (𝜓 → 𝜑)) |
8 | 2, 1, 7 | cbv3v 2325 | . 2 ⊢ (∀𝑦𝜓 → ∀𝑥𝜑) |
9 | 5, 8 | impbii 208 | 1 ⊢ (∀𝑥𝜑 ↔ ∀𝑦𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∀wal 1531 Ⅎwnf 1777 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-11 2146 ax-12 2166 |
This theorem depends on definitions: df-bi 206 df-an 395 df-ex 1774 df-nf 1778 |
This theorem is referenced by: cbvexv1 2332 cbval2v 2333 sb8fOLD 2344 sbbib 2351 cbvsbvf 2354 sb8eulem 2586 cbvmow 2591 abbib 2797 cleqh 2855 cleqf 2923 cbvralfw 3291 cbvralf 3343 ralab2 3689 cbvralcsf 3934 dfssf 3967 ab0OLD 4377 elintabOLD 4963 reusv2lem4 5401 cbviotaw 6508 cbviota 6511 sb8iota 6513 dffun6f 6567 findcard2 9189 findcard2OLD 9309 aceq1 10142 bnj1385 34594 sbcalf 37718 alrimii 37723 aomclem6 42625 rababg 43146 |
Copyright terms: Public domain | W3C validator |