![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > cbval | Structured version Visualization version GIF version |
Description: Rule used to change bound variables, using implicit substitution. (Contributed by NM, 13-May-1993.) (Revised by Mario Carneiro, 3-Oct-2016.) |
Ref | Expression |
---|---|
cbval.1 | ⊢ Ⅎ𝑦𝜑 |
cbval.2 | ⊢ Ⅎ𝑥𝜓 |
cbval.3 | ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) |
Ref | Expression |
---|---|
cbval | ⊢ (∀𝑥𝜑 ↔ ∀𝑦𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cbval.1 | . . 3 ⊢ Ⅎ𝑦𝜑 | |
2 | cbval.2 | . . 3 ⊢ Ⅎ𝑥𝜓 | |
3 | cbval.3 | . . . 4 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) | |
4 | 3 | biimpd 219 | . . 3 ⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓)) |
5 | 1, 2, 4 | cbv3 2301 | . 2 ⊢ (∀𝑥𝜑 → ∀𝑦𝜓) |
6 | 3 | biimprd 238 | . . . 4 ⊢ (𝑥 = 𝑦 → (𝜓 → 𝜑)) |
7 | 6 | equcoms 1993 | . . 3 ⊢ (𝑦 = 𝑥 → (𝜓 → 𝜑)) |
8 | 2, 1, 7 | cbv3 2301 | . 2 ⊢ (∀𝑦𝜓 → ∀𝑥𝜑) |
9 | 5, 8 | impbii 199 | 1 ⊢ (∀𝑥𝜑 ↔ ∀𝑦𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 196 ∀wal 1521 Ⅎwnf 1748 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1762 ax-4 1777 ax-5 1879 ax-6 1945 ax-7 1981 ax-10 2059 ax-11 2074 ax-12 2087 ax-13 2282 |
This theorem depends on definitions: df-bi 197 df-an 385 df-ex 1745 df-nf 1750 |
This theorem is referenced by: cbvex 2308 cbvalvOLD 2310 cbval2 2315 sb8 2452 sb8eu 2532 cbvralf 3195 ralab2 3404 cbvralcsf 3598 dfss2f 3627 elintab 4519 reusv2lem4 4902 cbviota 5894 sb8iota 5896 dffun6f 5940 findcard2 8241 aceq1 8978 bnj1385 31029 sbcalf 34047 alrimii 34054 aomclem6 37946 rababg 38196 |
Copyright terms: Public domain | W3C validator |