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 1412 | . 2 ⊢ (𝜑 → ∀𝑦𝜑) |
3 | cbval.2 | . . 3 ⊢ Ⅎ𝑥𝜓 | |
4 | 3 | nfri 1412 | . 2 ⊢ (𝜓 → ∀𝑥𝜓) |
5 | cbval.3 | . 2 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) | |
6 | 2, 4, 5 | cbvalh 1636 | 1 ⊢ (∀𝑥𝜑 ↔ ∀𝑦𝜓) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 98 ∀wal 1241 Ⅎwnf 1349 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 ax-5 1336 ax-7 1337 ax-gen 1338 ax-ie1 1382 ax-ie2 1383 ax-8 1395 ax-4 1400 ax-17 1419 ax-i9 1423 ax-ial 1427 |
This theorem depends on definitions: df-bi 110 df-nf 1350 |
This theorem is referenced by: sb8 1736 cbval2 1796 sb8eu 1913 abbi 2151 cleqf 2201 cbvralf 2527 ralab2 2705 cbvralcsf 2908 dfss2f 2936 elintab 3626 cbviota 4872 sb8iota 4874 dffun6f 4915 dffun4f 4918 mptfvex 5256 findcard2 6346 findcard2s 6347 |
Copyright terms: Public domain | W3C validator |