Proof of Theorem sbcpr
Step | Hyp | Ref
| Expression |
1 | | sbc5 3744 |
. . 3
⊢
([{𝑎, 𝑏} / 𝑝]𝜑 ↔ ∃𝑝(𝑝 = {𝑎, 𝑏} ∧ 𝜑)) |
2 | | preq12 4671 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 = 𝑎 ∧ 𝑦 = 𝑏) → {𝑥, 𝑦} = {𝑎, 𝑏}) |
3 | 2 | eqcomd 2744 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 = 𝑎 ∧ 𝑦 = 𝑏) → {𝑎, 𝑏} = {𝑥, 𝑦}) |
4 | 3 | eqeq2d 2749 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 = 𝑎 ∧ 𝑦 = 𝑏) → (𝑝 = {𝑎, 𝑏} ↔ 𝑝 = {𝑥, 𝑦})) |
5 | 4 | biimpa 477 |
. . . . . . . . . . . . . . 15
⊢ (((𝑥 = 𝑎 ∧ 𝑦 = 𝑏) ∧ 𝑝 = {𝑎, 𝑏}) → 𝑝 = {𝑥, 𝑦}) |
6 | | sbcpr.x |
. . . . . . . . . . . . . . 15
⊢ (𝑝 = {𝑥, 𝑦} → (𝜑 ↔ 𝜓)) |
7 | 5, 6 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 = 𝑎 ∧ 𝑦 = 𝑏) ∧ 𝑝 = {𝑎, 𝑏}) → (𝜑 ↔ 𝜓)) |
8 | 7 | biimpd 228 |
. . . . . . . . . . . . 13
⊢ (((𝑥 = 𝑎 ∧ 𝑦 = 𝑏) ∧ 𝑝 = {𝑎, 𝑏}) → (𝜑 → 𝜓)) |
9 | 8 | expcom 414 |
. . . . . . . . . . . 12
⊢ (𝑝 = {𝑎, 𝑏} → ((𝑥 = 𝑎 ∧ 𝑦 = 𝑏) → (𝜑 → 𝜓))) |
10 | 9 | expd 416 |
. . . . . . . . . . 11
⊢ (𝑝 = {𝑎, 𝑏} → (𝑥 = 𝑎 → (𝑦 = 𝑏 → (𝜑 → 𝜓)))) |
11 | 10 | com24 95 |
. . . . . . . . . 10
⊢ (𝑝 = {𝑎, 𝑏} → (𝜑 → (𝑦 = 𝑏 → (𝑥 = 𝑎 → 𝜓)))) |
12 | 11 | imp31 418 |
. . . . . . . . 9
⊢ (((𝑝 = {𝑎, 𝑏} ∧ 𝜑) ∧ 𝑦 = 𝑏) → (𝑥 = 𝑎 → 𝜓)) |
13 | 12 | alrimiv 1930 |
. . . . . . . 8
⊢ (((𝑝 = {𝑎, 𝑏} ∧ 𝜑) ∧ 𝑦 = 𝑏) → ∀𝑥(𝑥 = 𝑎 → 𝜓)) |
14 | | vex 3436 |
. . . . . . . . 9
⊢ 𝑎 ∈ V |
15 | 14 | sbc6 3748 |
. . . . . . . 8
⊢
([𝑎 / 𝑥]𝜓 ↔ ∀𝑥(𝑥 = 𝑎 → 𝜓)) |
16 | 13, 15 | sylibr 233 |
. . . . . . 7
⊢ (((𝑝 = {𝑎, 𝑏} ∧ 𝜑) ∧ 𝑦 = 𝑏) → [𝑎 / 𝑥]𝜓) |
17 | 16 | ex 413 |
. . . . . 6
⊢ ((𝑝 = {𝑎, 𝑏} ∧ 𝜑) → (𝑦 = 𝑏 → [𝑎 / 𝑥]𝜓)) |
18 | 17 | alrimiv 1930 |
. . . . 5
⊢ ((𝑝 = {𝑎, 𝑏} ∧ 𝜑) → ∀𝑦(𝑦 = 𝑏 → [𝑎 / 𝑥]𝜓)) |
19 | | vex 3436 |
. . . . . 6
⊢ 𝑏 ∈ V |
20 | 19 | sbc6 3748 |
. . . . 5
⊢
([𝑏 / 𝑦][𝑎 / 𝑥]𝜓 ↔ ∀𝑦(𝑦 = 𝑏 → [𝑎 / 𝑥]𝜓)) |
21 | 18, 20 | sylibr 233 |
. . . 4
⊢ ((𝑝 = {𝑎, 𝑏} ∧ 𝜑) → [𝑏 / 𝑦][𝑎 / 𝑥]𝜓) |
22 | 21 | exlimiv 1933 |
. . 3
⊢
(∃𝑝(𝑝 = {𝑎, 𝑏} ∧ 𝜑) → [𝑏 / 𝑦][𝑎 / 𝑥]𝜓) |
23 | 1, 22 | sylbi 216 |
. 2
⊢
([{𝑎, 𝑏} / 𝑝]𝜑 → [𝑏 / 𝑦][𝑎 / 𝑥]𝜓) |
24 | | sbc5 3744 |
. . . . 5
⊢
([𝑏 / 𝑦][𝑎 / 𝑥]𝜓 ↔ ∃𝑦(𝑦 = 𝑏 ∧ [𝑎 / 𝑥]𝜓)) |
25 | | sbc5 3744 |
. . . . . . . 8
⊢
([𝑎 / 𝑥]𝜓 ↔ ∃𝑥(𝑥 = 𝑎 ∧ 𝜓)) |
26 | 6 | bicomd 222 |
. . . . . . . . . . . . . . 15
⊢ (𝑝 = {𝑥, 𝑦} → (𝜓 ↔ 𝜑)) |
27 | 5, 26 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 = 𝑎 ∧ 𝑦 = 𝑏) ∧ 𝑝 = {𝑎, 𝑏}) → (𝜓 ↔ 𝜑)) |
28 | 27 | biimpd 228 |
. . . . . . . . . . . . 13
⊢ (((𝑥 = 𝑎 ∧ 𝑦 = 𝑏) ∧ 𝑝 = {𝑎, 𝑏}) → (𝜓 → 𝜑)) |
29 | 28 | expcom 414 |
. . . . . . . . . . . 12
⊢ (𝑝 = {𝑎, 𝑏} → ((𝑥 = 𝑎 ∧ 𝑦 = 𝑏) → (𝜓 → 𝜑))) |
30 | 29 | com13 88 |
. . . . . . . . . . 11
⊢ (𝜓 → ((𝑥 = 𝑎 ∧ 𝑦 = 𝑏) → (𝑝 = {𝑎, 𝑏} → 𝜑))) |
31 | 30 | expd 416 |
. . . . . . . . . 10
⊢ (𝜓 → (𝑥 = 𝑎 → (𝑦 = 𝑏 → (𝑝 = {𝑎, 𝑏} → 𝜑)))) |
32 | 31 | impcom 408 |
. . . . . . . . 9
⊢ ((𝑥 = 𝑎 ∧ 𝜓) → (𝑦 = 𝑏 → (𝑝 = {𝑎, 𝑏} → 𝜑))) |
33 | 32 | exlimiv 1933 |
. . . . . . . 8
⊢
(∃𝑥(𝑥 = 𝑎 ∧ 𝜓) → (𝑦 = 𝑏 → (𝑝 = {𝑎, 𝑏} → 𝜑))) |
34 | 25, 33 | sylbi 216 |
. . . . . . 7
⊢
([𝑎 / 𝑥]𝜓 → (𝑦 = 𝑏 → (𝑝 = {𝑎, 𝑏} → 𝜑))) |
35 | 34 | impcom 408 |
. . . . . 6
⊢ ((𝑦 = 𝑏 ∧ [𝑎 / 𝑥]𝜓) → (𝑝 = {𝑎, 𝑏} → 𝜑)) |
36 | 35 | exlimiv 1933 |
. . . . 5
⊢
(∃𝑦(𝑦 = 𝑏 ∧ [𝑎 / 𝑥]𝜓) → (𝑝 = {𝑎, 𝑏} → 𝜑)) |
37 | 24, 36 | sylbi 216 |
. . . 4
⊢
([𝑏 / 𝑦][𝑎 / 𝑥]𝜓 → (𝑝 = {𝑎, 𝑏} → 𝜑)) |
38 | 37 | alrimiv 1930 |
. . 3
⊢
([𝑏 / 𝑦][𝑎 / 𝑥]𝜓 → ∀𝑝(𝑝 = {𝑎, 𝑏} → 𝜑)) |
39 | | prex 5355 |
. . . 4
⊢ {𝑎, 𝑏} ∈ V |
40 | 39 | sbc6 3748 |
. . 3
⊢
([{𝑎, 𝑏} / 𝑝]𝜑 ↔ ∀𝑝(𝑝 = {𝑎, 𝑏} → 𝜑)) |
41 | 38, 40 | sylibr 233 |
. 2
⊢
([𝑏 / 𝑦][𝑎 / 𝑥]𝜓 → [{𝑎, 𝑏} / 𝑝]𝜑) |
42 | 23, 41 | impbii 208 |
1
⊢
([{𝑎, 𝑏} / 𝑝]𝜑 ↔ [𝑏 / 𝑦][𝑎 / 𝑥]𝜓) |