![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > cbvral | GIF version |
Description: Rule used to change bound variables, using implicit substitution. (Contributed by NM, 31-Jul-2003.) |
Ref | Expression |
---|---|
cbvral.1 | ⊢ Ⅎ𝑦𝜑 |
cbvral.2 | ⊢ Ⅎ𝑥𝜓 |
cbvral.3 | ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) |
Ref | Expression |
---|---|
cbvral | ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦 ∈ 𝐴 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfcv 2235 | . 2 ⊢ Ⅎ𝑥𝐴 | |
2 | nfcv 2235 | . 2 ⊢ Ⅎ𝑦𝐴 | |
3 | cbvral.1 | . 2 ⊢ Ⅎ𝑦𝜑 | |
4 | cbvral.2 | . 2 ⊢ Ⅎ𝑥𝜓 | |
5 | cbvral.3 | . 2 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) | |
6 | 1, 2, 3, 4, 5 | cbvralf 2598 | 1 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦 ∈ 𝐴 𝜓) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 104 Ⅎwnf 1401 ∀wral 2370 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-io 668 ax-5 1388 ax-7 1389 ax-gen 1390 ax-ie1 1434 ax-ie2 1435 ax-8 1447 ax-10 1448 ax-11 1449 ax-i12 1450 ax-bndl 1451 ax-4 1452 ax-17 1471 ax-i9 1475 ax-ial 1479 ax-i5r 1480 ax-ext 2077 |
This theorem depends on definitions: df-bi 116 df-nf 1402 df-sb 1700 df-cleq 2088 df-clel 2091 df-nfc 2224 df-ral 2375 |
This theorem is referenced by: cbvralv 2604 cbvralsv 2615 cbviin 3790 frind 4203 ralxpf 4613 eqfnfv2f 5440 ralrnmpt 5480 dff13f 5587 ofrfval2 5909 fmpt2x 6008 cbvixp 6512 mptelixpg 6531 xpf1o 6640 indstr 9180 fsum3 10946 fsum00 11021 mertenslem2 11095 cnmpt11 12121 bj-bdfindes 12568 bj-findes 12600 |
Copyright terms: Public domain | W3C validator |