![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > sbralie | GIF version |
Description: Implicit to explicit substitution that swaps variables in a quantified expression. (Contributed by NM, 5-Sep-2004.) |
Ref | Expression |
---|---|
sbralie.1 | ⊢ (x = y → (φ ↔ ψ)) |
Ref | Expression |
---|---|
sbralie | ⊢ ([x / y]∀x ∈ y φ ↔ ∀y ∈ x ψ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cbvralsv 2538 | . . . 4 ⊢ (∀x ∈ y φ ↔ ∀z ∈ y [z / x]φ) | |
2 | 1 | sbbii 1645 | . . 3 ⊢ ([x / y]∀x ∈ y φ ↔ [x / y]∀z ∈ y [z / x]φ) |
3 | nfv 1418 | . . . 4 ⊢ Ⅎy∀z ∈ x [z / x]φ | |
4 | raleq 2499 | . . . 4 ⊢ (y = x → (∀z ∈ y [z / x]φ ↔ ∀z ∈ x [z / x]φ)) | |
5 | 3, 4 | sbie 1671 | . . 3 ⊢ ([x / y]∀z ∈ y [z / x]φ ↔ ∀z ∈ x [z / x]φ) |
6 | 2, 5 | bitri 173 | . 2 ⊢ ([x / y]∀x ∈ y φ ↔ ∀z ∈ x [z / x]φ) |
7 | cbvralsv 2538 | . . 3 ⊢ (∀z ∈ x [z / x]φ ↔ ∀y ∈ x [y / z][z / x]φ) | |
8 | nfv 1418 | . . . . . 6 ⊢ Ⅎzφ | |
9 | 8 | sbco2 1836 | . . . . 5 ⊢ ([y / z][z / x]φ ↔ [y / x]φ) |
10 | nfv 1418 | . . . . . 6 ⊢ Ⅎxψ | |
11 | sbralie.1 | . . . . . 6 ⊢ (x = y → (φ ↔ ψ)) | |
12 | 10, 11 | sbie 1671 | . . . . 5 ⊢ ([y / x]φ ↔ ψ) |
13 | 9, 12 | bitri 173 | . . . 4 ⊢ ([y / z][z / x]φ ↔ ψ) |
14 | 13 | ralbii 2324 | . . 3 ⊢ (∀y ∈ x [y / z][z / x]φ ↔ ∀y ∈ x ψ) |
15 | 7, 14 | bitri 173 | . 2 ⊢ (∀z ∈ x [z / x]φ ↔ ∀y ∈ x ψ) |
16 | 6, 15 | bitri 173 | 1 ⊢ ([x / y]∀x ∈ y φ ↔ ∀y ∈ x ψ) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 98 [wsb 1642 ∀wral 2300 |
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-io 629 ax-5 1333 ax-7 1334 ax-gen 1335 ax-ie1 1379 ax-ie2 1380 ax-8 1392 ax-10 1393 ax-11 1394 ax-i12 1395 ax-bndl 1396 ax-4 1397 ax-17 1416 ax-i9 1420 ax-ial 1424 ax-i5r 1425 ax-ext 2019 |
This theorem depends on definitions: df-bi 110 df-tru 1245 df-nf 1347 df-sb 1643 df-cleq 2030 df-clel 2033 df-nfc 2164 df-ral 2305 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |