![]() |
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 2410 | . 2 ⊢ (∀𝑥𝜑 → ∀𝑦𝜓) |
6 | 3 | biimprd 238 | . . . 4 ⊢ (𝑥 = 𝑦 → (𝜓 → 𝜑)) |
7 | 6 | equcoms 2102 | . . 3 ⊢ (𝑦 = 𝑥 → (𝜓 → 𝜑)) |
8 | 2, 1, 7 | cbv3 2410 | . 2 ⊢ (∀𝑦𝜓 → ∀𝑥𝜑) |
9 | 5, 8 | impbii 199 | 1 ⊢ (∀𝑥𝜑 ↔ ∀𝑦𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 196 ∀wal 1630 Ⅎwnf 1857 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1871 ax-4 1886 ax-5 1988 ax-6 2054 ax-7 2090 ax-10 2168 ax-11 2183 ax-12 2196 ax-13 2391 |
This theorem depends on definitions: df-bi 197 df-an 385 df-ex 1854 df-nf 1859 |
This theorem is referenced by: cbvex 2417 cbvalvOLD 2419 cbval2 2424 sb8 2561 sb8eu 2641 cbvralf 3304 ralab2 3512 cbvralcsf 3706 dfss2f 3735 elintab 4639 reusv2lem4 5021 cbviota 6017 sb8iota 6019 dffun6f 6063 findcard2 8367 aceq1 9150 bnj1385 31231 sbcalf 34248 alrimii 34255 aomclem6 38149 rababg 38399 |
Copyright terms: Public domain | W3C validator |