Proof of Theorem sbcrextOLD
Step | Hyp | Ref
| Expression |
1 | | sbcng 3443 |
. . . . 5
⊢ (𝐴 ∈ V → ([𝐴 / 𝑥] ¬ ∀𝑦 ∈ 𝐵 ¬ 𝜑 ↔ ¬ [𝐴 / 𝑥]∀𝑦 ∈ 𝐵 ¬ 𝜑)) |
2 | 1 | adantr 480 |
. . . 4
⊢ ((𝐴 ∈ V ∧
Ⅎ𝑦𝐴) → ([𝐴 / 𝑥] ¬ ∀𝑦 ∈ 𝐵 ¬ 𝜑 ↔ ¬ [𝐴 / 𝑥]∀𝑦 ∈ 𝐵 ¬ 𝜑)) |
3 | | sbcralt 3477 |
. . . . . 6
⊢ ((𝐴 ∈ V ∧
Ⅎ𝑦𝐴) → ([𝐴 / 𝑥]∀𝑦 ∈ 𝐵 ¬ 𝜑 ↔ ∀𝑦 ∈ 𝐵 [𝐴 / 𝑥] ¬ 𝜑)) |
4 | | nfnfc1 2754 |
. . . . . . . . 9
⊢
Ⅎ𝑦Ⅎ𝑦𝐴 |
5 | | id 22 |
. . . . . . . . . 10
⊢
(Ⅎ𝑦𝐴 → Ⅎ𝑦𝐴) |
6 | | nfcvd 2752 |
. . . . . . . . . 10
⊢
(Ⅎ𝑦𝐴 → Ⅎ𝑦V) |
7 | 5, 6 | nfeld 2759 |
. . . . . . . . 9
⊢
(Ⅎ𝑦𝐴 → Ⅎ𝑦 𝐴 ∈ V) |
8 | 4, 7 | nfan1 2056 |
. . . . . . . 8
⊢
Ⅎ𝑦(Ⅎ𝑦𝐴 ∧ 𝐴 ∈ V) |
9 | | sbcng 3443 |
. . . . . . . . 9
⊢ (𝐴 ∈ V → ([𝐴 / 𝑥] ¬ 𝜑 ↔ ¬ [𝐴 / 𝑥]𝜑)) |
10 | 9 | adantl 481 |
. . . . . . . 8
⊢
((Ⅎ𝑦𝐴 ∧ 𝐴 ∈ V) → ([𝐴 / 𝑥] ¬ 𝜑 ↔ ¬ [𝐴 / 𝑥]𝜑)) |
11 | 8, 10 | ralbid 2966 |
. . . . . . 7
⊢
((Ⅎ𝑦𝐴 ∧ 𝐴 ∈ V) → (∀𝑦 ∈ 𝐵 [𝐴 / 𝑥] ¬ 𝜑 ↔ ∀𝑦 ∈ 𝐵 ¬ [𝐴 / 𝑥]𝜑)) |
12 | 11 | ancoms 468 |
. . . . . 6
⊢ ((𝐴 ∈ V ∧
Ⅎ𝑦𝐴) → (∀𝑦 ∈ 𝐵 [𝐴 / 𝑥] ¬ 𝜑 ↔ ∀𝑦 ∈ 𝐵 ¬ [𝐴 / 𝑥]𝜑)) |
13 | 3, 12 | bitrd 267 |
. . . . 5
⊢ ((𝐴 ∈ V ∧
Ⅎ𝑦𝐴) → ([𝐴 / 𝑥]∀𝑦 ∈ 𝐵 ¬ 𝜑 ↔ ∀𝑦 ∈ 𝐵 ¬ [𝐴 / 𝑥]𝜑)) |
14 | 13 | notbid 307 |
. . . 4
⊢ ((𝐴 ∈ V ∧
Ⅎ𝑦𝐴) → (¬ [𝐴 / 𝑥]∀𝑦 ∈ 𝐵 ¬ 𝜑 ↔ ¬ ∀𝑦 ∈ 𝐵 ¬ [𝐴 / 𝑥]𝜑)) |
15 | 2, 14 | bitrd 267 |
. . 3
⊢ ((𝐴 ∈ V ∧
Ⅎ𝑦𝐴) → ([𝐴 / 𝑥] ¬ ∀𝑦 ∈ 𝐵 ¬ 𝜑 ↔ ¬ ∀𝑦 ∈ 𝐵 ¬ [𝐴 / 𝑥]𝜑)) |
16 | | dfrex2 2979 |
. . . 4
⊢
(∃𝑦 ∈
𝐵 𝜑 ↔ ¬ ∀𝑦 ∈ 𝐵 ¬ 𝜑) |
17 | 16 | sbcbii 3458 |
. . 3
⊢
([𝐴 / 𝑥]∃𝑦 ∈ 𝐵 𝜑 ↔ [𝐴 / 𝑥] ¬ ∀𝑦 ∈ 𝐵 ¬ 𝜑) |
18 | | dfrex2 2979 |
. . 3
⊢
(∃𝑦 ∈
𝐵 [𝐴 / 𝑥]𝜑 ↔ ¬ ∀𝑦 ∈ 𝐵 ¬ [𝐴 / 𝑥]𝜑) |
19 | 15, 17, 18 | 3bitr4g 302 |
. 2
⊢ ((𝐴 ∈ V ∧
Ⅎ𝑦𝐴) → ([𝐴 / 𝑥]∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑦 ∈ 𝐵 [𝐴 / 𝑥]𝜑)) |
20 | | sbcex 3412 |
. . . . 5
⊢
([𝐴 / 𝑥]∃𝑦 ∈ 𝐵 𝜑 → 𝐴 ∈ V) |
21 | 20 | con3i 149 |
. . . 4
⊢ (¬
𝐴 ∈ V → ¬
[𝐴 / 𝑥]∃𝑦 ∈ 𝐵 𝜑) |
22 | 21 | adantr 480 |
. . 3
⊢ ((¬
𝐴 ∈ V ∧
Ⅎ𝑦𝐴) → ¬ [𝐴 / 𝑥]∃𝑦 ∈ 𝐵 𝜑) |
23 | | sbcex 3412 |
. . . . . . 7
⊢
([𝐴 / 𝑥]𝜑 → 𝐴 ∈ V) |
24 | 23 | 2a1i 12 |
. . . . . 6
⊢
(Ⅎ𝑦𝐴 → (𝑦 ∈ 𝐵 → ([𝐴 / 𝑥]𝜑 → 𝐴 ∈ V))) |
25 | 4, 7, 24 | rexlimd2 3007 |
. . . . 5
⊢
(Ⅎ𝑦𝐴 → (∃𝑦 ∈ 𝐵 [𝐴 / 𝑥]𝜑 → 𝐴 ∈ V)) |
26 | 25 | con3rr3 150 |
. . . 4
⊢ (¬
𝐴 ∈ V →
(Ⅎ𝑦𝐴 → ¬ ∃𝑦 ∈ 𝐵 [𝐴 / 𝑥]𝜑)) |
27 | 26 | imp 444 |
. . 3
⊢ ((¬
𝐴 ∈ V ∧
Ⅎ𝑦𝐴) → ¬ ∃𝑦 ∈ 𝐵 [𝐴 / 𝑥]𝜑) |
28 | 22, 27 | 2falsed 365 |
. 2
⊢ ((¬
𝐴 ∈ V ∧
Ⅎ𝑦𝐴) → ([𝐴 / 𝑥]∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑦 ∈ 𝐵 [𝐴 / 𝑥]𝜑)) |
29 | 19, 28 | pm2.61ian 827 |
1
⊢
(Ⅎ𝑦𝐴 → ([𝐴 / 𝑥]∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑦 ∈ 𝐵 [𝐴 / 𝑥]𝜑)) |