![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > cbvex2 | GIF version |
Description: Rule used to change bound variables, using implicit substitution. (Contributed by NM, 14-Sep-2003.) (Revised by Mario Carneiro, 6-Oct-2016.) |
Ref | Expression |
---|---|
cbval2.1 | ⊢ Ⅎ𝑧𝜑 |
cbval2.2 | ⊢ Ⅎ𝑤𝜑 |
cbval2.3 | ⊢ Ⅎ𝑥𝜓 |
cbval2.4 | ⊢ Ⅎ𝑦𝜓 |
cbval2.5 | ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (𝜑 ↔ 𝜓)) |
Ref | Expression |
---|---|
cbvex2 | ⊢ (∃𝑥∃𝑦𝜑 ↔ ∃𝑧∃𝑤𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cbval2.1 | . . 3 ⊢ Ⅎ𝑧𝜑 | |
2 | 1 | nfex 1637 | . 2 ⊢ Ⅎ𝑧∃𝑦𝜑 |
3 | cbval2.3 | . . 3 ⊢ Ⅎ𝑥𝜓 | |
4 | 3 | nfex 1637 | . 2 ⊢ Ⅎ𝑥∃𝑤𝜓 |
5 | nfv 1528 | . . . . . 6 ⊢ Ⅎ𝑤 𝑥 = 𝑧 | |
6 | cbval2.2 | . . . . . 6 ⊢ Ⅎ𝑤𝜑 | |
7 | 5, 6 | nfan 1565 | . . . . 5 ⊢ Ⅎ𝑤(𝑥 = 𝑧 ∧ 𝜑) |
8 | nfv 1528 | . . . . . 6 ⊢ Ⅎ𝑦 𝑥 = 𝑧 | |
9 | cbval2.4 | . . . . . 6 ⊢ Ⅎ𝑦𝜓 | |
10 | 8, 9 | nfan 1565 | . . . . 5 ⊢ Ⅎ𝑦(𝑥 = 𝑧 ∧ 𝜓) |
11 | cbval2.5 | . . . . . . 7 ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (𝜑 ↔ 𝜓)) | |
12 | 11 | expcom 116 | . . . . . 6 ⊢ (𝑦 = 𝑤 → (𝑥 = 𝑧 → (𝜑 ↔ 𝜓))) |
13 | 12 | pm5.32d 450 | . . . . 5 ⊢ (𝑦 = 𝑤 → ((𝑥 = 𝑧 ∧ 𝜑) ↔ (𝑥 = 𝑧 ∧ 𝜓))) |
14 | 7, 10, 13 | cbvex 1756 | . . . 4 ⊢ (∃𝑦(𝑥 = 𝑧 ∧ 𝜑) ↔ ∃𝑤(𝑥 = 𝑧 ∧ 𝜓)) |
15 | 19.42v 1906 | . . . 4 ⊢ (∃𝑦(𝑥 = 𝑧 ∧ 𝜑) ↔ (𝑥 = 𝑧 ∧ ∃𝑦𝜑)) | |
16 | 19.42v 1906 | . . . 4 ⊢ (∃𝑤(𝑥 = 𝑧 ∧ 𝜓) ↔ (𝑥 = 𝑧 ∧ ∃𝑤𝜓)) | |
17 | 14, 15, 16 | 3bitr3i 210 | . . 3 ⊢ ((𝑥 = 𝑧 ∧ ∃𝑦𝜑) ↔ (𝑥 = 𝑧 ∧ ∃𝑤𝜓)) |
18 | pm5.32 453 | . . 3 ⊢ ((𝑥 = 𝑧 → (∃𝑦𝜑 ↔ ∃𝑤𝜓)) ↔ ((𝑥 = 𝑧 ∧ ∃𝑦𝜑) ↔ (𝑥 = 𝑧 ∧ ∃𝑤𝜓))) | |
19 | 17, 18 | mpbir 146 | . 2 ⊢ (𝑥 = 𝑧 → (∃𝑦𝜑 ↔ ∃𝑤𝜓)) |
20 | 2, 4, 19 | cbvex 1756 | 1 ⊢ (∃𝑥∃𝑦𝜑 ↔ ∃𝑧∃𝑤𝜓) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 104 ↔ wb 105 Ⅎwnf 1460 ∃wex 1492 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-5 1447 ax-7 1448 ax-gen 1449 ax-ie1 1493 ax-ie2 1494 ax-8 1504 ax-4 1510 ax-17 1526 ax-i9 1530 ax-ial 1534 |
This theorem depends on definitions: df-bi 117 df-nf 1461 |
This theorem is referenced by: cbvex2v 1924 cbvopab 4075 cbvoprab12 5949 |
Copyright terms: Public domain | W3C validator |