Proof of Theorem sbcpr
| Step | Hyp | Ref
| Expression |
| 1 | | sbc5 3816 |
. . 3
⊢
([{𝑎, 𝑏} / 𝑝]𝜑 ↔ ∃𝑝(𝑝 = {𝑎, 𝑏} ∧ 𝜑)) |
| 2 | | preq12 4735 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 = 𝑎 ∧ 𝑦 = 𝑏) → {𝑥, 𝑦} = {𝑎, 𝑏}) |
| 3 | 2 | eqcomd 2743 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 = 𝑎 ∧ 𝑦 = 𝑏) → {𝑎, 𝑏} = {𝑥, 𝑦}) |
| 4 | 3 | eqeq2d 2748 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 = 𝑎 ∧ 𝑦 = 𝑏) → (𝑝 = {𝑎, 𝑏} ↔ 𝑝 = {𝑥, 𝑦})) |
| 5 | 4 | biimpa 476 |
. . . . . . . . . . . . . . 15
⊢ (((𝑥 = 𝑎 ∧ 𝑦 = 𝑏) ∧ 𝑝 = {𝑎, 𝑏}) → 𝑝 = {𝑥, 𝑦}) |
| 6 | | sbcpr.x |
. . . . . . . . . . . . . . 15
⊢ (𝑝 = {𝑥, 𝑦} → (𝜑 ↔ 𝜓)) |
| 7 | 5, 6 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 = 𝑎 ∧ 𝑦 = 𝑏) ∧ 𝑝 = {𝑎, 𝑏}) → (𝜑 ↔ 𝜓)) |
| 8 | 7 | biimpd 229 |
. . . . . . . . . . . . 13
⊢ (((𝑥 = 𝑎 ∧ 𝑦 = 𝑏) ∧ 𝑝 = {𝑎, 𝑏}) → (𝜑 → 𝜓)) |
| 9 | 8 | expcom 413 |
. . . . . . . . . . . 12
⊢ (𝑝 = {𝑎, 𝑏} → ((𝑥 = 𝑎 ∧ 𝑦 = 𝑏) → (𝜑 → 𝜓))) |
| 10 | 9 | expd 415 |
. . . . . . . . . . 11
⊢ (𝑝 = {𝑎, 𝑏} → (𝑥 = 𝑎 → (𝑦 = 𝑏 → (𝜑 → 𝜓)))) |
| 11 | 10 | com24 95 |
. . . . . . . . . 10
⊢ (𝑝 = {𝑎, 𝑏} → (𝜑 → (𝑦 = 𝑏 → (𝑥 = 𝑎 → 𝜓)))) |
| 12 | 11 | imp31 417 |
. . . . . . . . 9
⊢ (((𝑝 = {𝑎, 𝑏} ∧ 𝜑) ∧ 𝑦 = 𝑏) → (𝑥 = 𝑎 → 𝜓)) |
| 13 | 12 | alrimiv 1927 |
. . . . . . . 8
⊢ (((𝑝 = {𝑎, 𝑏} ∧ 𝜑) ∧ 𝑦 = 𝑏) → ∀𝑥(𝑥 = 𝑎 → 𝜓)) |
| 14 | | vex 3484 |
. . . . . . . . 9
⊢ 𝑎 ∈ V |
| 15 | 14 | sbc6 3819 |
. . . . . . . 8
⊢
([𝑎 / 𝑥]𝜓 ↔ ∀𝑥(𝑥 = 𝑎 → 𝜓)) |
| 16 | 13, 15 | sylibr 234 |
. . . . . . 7
⊢ (((𝑝 = {𝑎, 𝑏} ∧ 𝜑) ∧ 𝑦 = 𝑏) → [𝑎 / 𝑥]𝜓) |
| 17 | 16 | ex 412 |
. . . . . 6
⊢ ((𝑝 = {𝑎, 𝑏} ∧ 𝜑) → (𝑦 = 𝑏 → [𝑎 / 𝑥]𝜓)) |
| 18 | 17 | alrimiv 1927 |
. . . . 5
⊢ ((𝑝 = {𝑎, 𝑏} ∧ 𝜑) → ∀𝑦(𝑦 = 𝑏 → [𝑎 / 𝑥]𝜓)) |
| 19 | | vex 3484 |
. . . . . 6
⊢ 𝑏 ∈ V |
| 20 | 19 | sbc6 3819 |
. . . . 5
⊢
([𝑏 / 𝑦][𝑎 / 𝑥]𝜓 ↔ ∀𝑦(𝑦 = 𝑏 → [𝑎 / 𝑥]𝜓)) |
| 21 | 18, 20 | sylibr 234 |
. . . 4
⊢ ((𝑝 = {𝑎, 𝑏} ∧ 𝜑) → [𝑏 / 𝑦][𝑎 / 𝑥]𝜓) |
| 22 | 21 | exlimiv 1930 |
. . 3
⊢
(∃𝑝(𝑝 = {𝑎, 𝑏} ∧ 𝜑) → [𝑏 / 𝑦][𝑎 / 𝑥]𝜓) |
| 23 | 1, 22 | sylbi 217 |
. 2
⊢
([{𝑎, 𝑏} / 𝑝]𝜑 → [𝑏 / 𝑦][𝑎 / 𝑥]𝜓) |
| 24 | | sbc5 3816 |
. . . . 5
⊢
([𝑏 / 𝑦][𝑎 / 𝑥]𝜓 ↔ ∃𝑦(𝑦 = 𝑏 ∧ [𝑎 / 𝑥]𝜓)) |
| 25 | | sbc5 3816 |
. . . . . . . 8
⊢
([𝑎 / 𝑥]𝜓 ↔ ∃𝑥(𝑥 = 𝑎 ∧ 𝜓)) |
| 26 | 6 | bicomd 223 |
. . . . . . . . . . . . . . 15
⊢ (𝑝 = {𝑥, 𝑦} → (𝜓 ↔ 𝜑)) |
| 27 | 5, 26 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 = 𝑎 ∧ 𝑦 = 𝑏) ∧ 𝑝 = {𝑎, 𝑏}) → (𝜓 ↔ 𝜑)) |
| 28 | 27 | biimpd 229 |
. . . . . . . . . . . . 13
⊢ (((𝑥 = 𝑎 ∧ 𝑦 = 𝑏) ∧ 𝑝 = {𝑎, 𝑏}) → (𝜓 → 𝜑)) |
| 29 | 28 | expcom 413 |
. . . . . . . . . . . 12
⊢ (𝑝 = {𝑎, 𝑏} → ((𝑥 = 𝑎 ∧ 𝑦 = 𝑏) → (𝜓 → 𝜑))) |
| 30 | 29 | com13 88 |
. . . . . . . . . . 11
⊢ (𝜓 → ((𝑥 = 𝑎 ∧ 𝑦 = 𝑏) → (𝑝 = {𝑎, 𝑏} → 𝜑))) |
| 31 | 30 | expd 415 |
. . . . . . . . . 10
⊢ (𝜓 → (𝑥 = 𝑎 → (𝑦 = 𝑏 → (𝑝 = {𝑎, 𝑏} → 𝜑)))) |
| 32 | 31 | impcom 407 |
. . . . . . . . 9
⊢ ((𝑥 = 𝑎 ∧ 𝜓) → (𝑦 = 𝑏 → (𝑝 = {𝑎, 𝑏} → 𝜑))) |
| 33 | 32 | exlimiv 1930 |
. . . . . . . 8
⊢
(∃𝑥(𝑥 = 𝑎 ∧ 𝜓) → (𝑦 = 𝑏 → (𝑝 = {𝑎, 𝑏} → 𝜑))) |
| 34 | 25, 33 | sylbi 217 |
. . . . . . 7
⊢
([𝑎 / 𝑥]𝜓 → (𝑦 = 𝑏 → (𝑝 = {𝑎, 𝑏} → 𝜑))) |
| 35 | 34 | impcom 407 |
. . . . . 6
⊢ ((𝑦 = 𝑏 ∧ [𝑎 / 𝑥]𝜓) → (𝑝 = {𝑎, 𝑏} → 𝜑)) |
| 36 | 35 | exlimiv 1930 |
. . . . 5
⊢
(∃𝑦(𝑦 = 𝑏 ∧ [𝑎 / 𝑥]𝜓) → (𝑝 = {𝑎, 𝑏} → 𝜑)) |
| 37 | 24, 36 | sylbi 217 |
. . . 4
⊢
([𝑏 / 𝑦][𝑎 / 𝑥]𝜓 → (𝑝 = {𝑎, 𝑏} → 𝜑)) |
| 38 | 37 | alrimiv 1927 |
. . 3
⊢
([𝑏 / 𝑦][𝑎 / 𝑥]𝜓 → ∀𝑝(𝑝 = {𝑎, 𝑏} → 𝜑)) |
| 39 | | prex 5437 |
. . . 4
⊢ {𝑎, 𝑏} ∈ V |
| 40 | 39 | sbc6 3819 |
. . 3
⊢
([{𝑎, 𝑏} / 𝑝]𝜑 ↔ ∀𝑝(𝑝 = {𝑎, 𝑏} → 𝜑)) |
| 41 | 38, 40 | sylibr 234 |
. 2
⊢
([𝑏 / 𝑦][𝑎 / 𝑥]𝜓 → [{𝑎, 𝑏} / 𝑝]𝜑) |
| 42 | 23, 41 | impbii 209 |
1
⊢
([{𝑎, 𝑏} / 𝑝]𝜑 ↔ [𝑏 / 𝑦][𝑎 / 𝑥]𝜓) |