Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > cbval | GIF version |
Description: Rule used to change bound variables, using implicit substitution. (Contributed by NM, 5-Aug-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 | 1 | nfri 1512 | . 2 ⊢ (𝜑 → ∀𝑦𝜑) |
3 | cbval.2 | . . 3 ⊢ Ⅎ𝑥𝜓 | |
4 | 3 | nfri 1512 | . 2 ⊢ (𝜓 → ∀𝑥𝜓) |
5 | cbval.3 | . 2 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) | |
6 | 2, 4, 5 | cbvalh 1746 | 1 ⊢ (∀𝑥𝜑 ↔ ∀𝑦𝜓) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 104 ∀wal 1346 Ⅎwnf 1453 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-5 1440 ax-7 1441 ax-gen 1442 ax-ie1 1486 ax-ie2 1487 ax-8 1497 ax-4 1503 ax-17 1519 ax-i9 1523 ax-ial 1527 |
This theorem depends on definitions: df-bi 116 df-nf 1454 |
This theorem is referenced by: sb8 1849 cbval2 1914 sb8eu 2032 abbi 2284 cleqf 2337 cbvralf 2689 ralab2 2894 cbvralcsf 3111 dfss2f 3138 elintab 3840 cbviota 5163 sb8iota 5165 dffun6f 5209 dffun4f 5212 mptfvex 5579 findcard2 6865 findcard2s 6866 |
Copyright terms: Public domain | W3C validator |