Proof of Theorem sbcrextOLD
Step | Hyp | Ref
| Expression |
1 | | sbcng 3476 |
. . . . 5
⊢ (𝐴 ∈ V → ([𝐴 / 𝑥] ¬ ∀𝑦 ∈ 𝐵 ¬ 𝜑 ↔ ¬ [𝐴 / 𝑥]∀𝑦 ∈ 𝐵 ¬ 𝜑)) |
2 | 1 | adantr 481 |
. . . 4
⊢ ((𝐴 ∈ V ∧
Ⅎ𝑦𝐴) → ([𝐴 / 𝑥] ¬ ∀𝑦 ∈ 𝐵 ¬ 𝜑 ↔ ¬ [𝐴 / 𝑥]∀𝑦 ∈ 𝐵 ¬ 𝜑)) |
3 | | sbcralt 3510 |
. . . . . 6
⊢ ((𝐴 ∈ V ∧
Ⅎ𝑦𝐴) → ([𝐴 / 𝑥]∀𝑦 ∈ 𝐵 ¬ 𝜑 ↔ ∀𝑦 ∈ 𝐵 [𝐴 / 𝑥] ¬ 𝜑)) |
4 | | nfnfc1 2767 |
. . . . . . . . 9
⊢
Ⅎ𝑦Ⅎ𝑦𝐴 |
5 | | id 22 |
. . . . . . . . . 10
⊢
(Ⅎ𝑦𝐴 → Ⅎ𝑦𝐴) |
6 | | nfcvd 2765 |
. . . . . . . . . 10
⊢
(Ⅎ𝑦𝐴 → Ⅎ𝑦V) |
7 | 5, 6 | nfeld 2773 |
. . . . . . . . 9
⊢
(Ⅎ𝑦𝐴 → Ⅎ𝑦 𝐴 ∈ V) |
8 | 4, 7 | nfan1 2068 |
. . . . . . . 8
⊢
Ⅎ𝑦(Ⅎ𝑦𝐴 ∧ 𝐴 ∈ V) |
9 | | sbcng 3476 |
. . . . . . . . 9
⊢ (𝐴 ∈ V → ([𝐴 / 𝑥] ¬ 𝜑 ↔ ¬ [𝐴 / 𝑥]𝜑)) |
10 | 9 | adantl 482 |
. . . . . . . 8
⊢
((Ⅎ𝑦𝐴 ∧ 𝐴 ∈ V) → ([𝐴 / 𝑥] ¬ 𝜑 ↔ ¬ [𝐴 / 𝑥]𝜑)) |
11 | 8, 10 | ralbid 2983 |
. . . . . . 7
⊢
((Ⅎ𝑦𝐴 ∧ 𝐴 ∈ V) → (∀𝑦 ∈ 𝐵 [𝐴 / 𝑥] ¬ 𝜑 ↔ ∀𝑦 ∈ 𝐵 ¬ [𝐴 / 𝑥]𝜑)) |
12 | 11 | ancoms 469 |
. . . . . 6
⊢ ((𝐴 ∈ V ∧
Ⅎ𝑦𝐴) → (∀𝑦 ∈ 𝐵 [𝐴 / 𝑥] ¬ 𝜑 ↔ ∀𝑦 ∈ 𝐵 ¬ [𝐴 / 𝑥]𝜑)) |
13 | 3, 12 | bitrd 268 |
. . . . 5
⊢ ((𝐴 ∈ V ∧
Ⅎ𝑦𝐴) → ([𝐴 / 𝑥]∀𝑦 ∈ 𝐵 ¬ 𝜑 ↔ ∀𝑦 ∈ 𝐵 ¬ [𝐴 / 𝑥]𝜑)) |
14 | 13 | notbid 308 |
. . . 4
⊢ ((𝐴 ∈ V ∧
Ⅎ𝑦𝐴) → (¬ [𝐴 / 𝑥]∀𝑦 ∈ 𝐵 ¬ 𝜑 ↔ ¬ ∀𝑦 ∈ 𝐵 ¬ [𝐴 / 𝑥]𝜑)) |
15 | 2, 14 | bitrd 268 |
. . 3
⊢ ((𝐴 ∈ V ∧
Ⅎ𝑦𝐴) → ([𝐴 / 𝑥] ¬ ∀𝑦 ∈ 𝐵 ¬ 𝜑 ↔ ¬ ∀𝑦 ∈ 𝐵 ¬ [𝐴 / 𝑥]𝜑)) |
16 | | dfrex2 2996 |
. . . 4
⊢
(∃𝑦 ∈
𝐵 𝜑 ↔ ¬ ∀𝑦 ∈ 𝐵 ¬ 𝜑) |
17 | 16 | sbcbii 3491 |
. . 3
⊢
([𝐴 / 𝑥]∃𝑦 ∈ 𝐵 𝜑 ↔ [𝐴 / 𝑥] ¬ ∀𝑦 ∈ 𝐵 ¬ 𝜑) |
18 | | dfrex2 2996 |
. . 3
⊢
(∃𝑦 ∈
𝐵 [𝐴 / 𝑥]𝜑 ↔ ¬ ∀𝑦 ∈ 𝐵 ¬ [𝐴 / 𝑥]𝜑) |
19 | 15, 17, 18 | 3bitr4g 303 |
. 2
⊢ ((𝐴 ∈ V ∧
Ⅎ𝑦𝐴) → ([𝐴 / 𝑥]∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑦 ∈ 𝐵 [𝐴 / 𝑥]𝜑)) |
20 | | sbcex 3445 |
. . . . 5
⊢
([𝐴 / 𝑥]∃𝑦 ∈ 𝐵 𝜑 → 𝐴 ∈ V) |
21 | 20 | con3i 150 |
. . . 4
⊢ (¬
𝐴 ∈ V → ¬
[𝐴 / 𝑥]∃𝑦 ∈ 𝐵 𝜑) |
22 | 21 | adantr 481 |
. . 3
⊢ ((¬
𝐴 ∈ V ∧
Ⅎ𝑦𝐴) → ¬ [𝐴 / 𝑥]∃𝑦 ∈ 𝐵 𝜑) |
23 | | sbcex 3445 |
. . . . . . 7
⊢
([𝐴 / 𝑥]𝜑 → 𝐴 ∈ V) |
24 | 23 | 2a1i 12 |
. . . . . 6
⊢
(Ⅎ𝑦𝐴 → (𝑦 ∈ 𝐵 → ([𝐴 / 𝑥]𝜑 → 𝐴 ∈ V))) |
25 | 4, 7, 24 | rexlimd2 3025 |
. . . . 5
⊢
(Ⅎ𝑦𝐴 → (∃𝑦 ∈ 𝐵 [𝐴 / 𝑥]𝜑 → 𝐴 ∈ V)) |
26 | 25 | con3rr3 151 |
. . . 4
⊢ (¬
𝐴 ∈ V →
(Ⅎ𝑦𝐴 → ¬ ∃𝑦 ∈ 𝐵 [𝐴 / 𝑥]𝜑)) |
27 | 26 | imp 445 |
. . 3
⊢ ((¬
𝐴 ∈ V ∧
Ⅎ𝑦𝐴) → ¬ ∃𝑦 ∈ 𝐵 [𝐴 / 𝑥]𝜑) |
28 | 22, 27 | 2falsed 366 |
. 2
⊢ ((¬
𝐴 ∈ V ∧
Ⅎ𝑦𝐴) → ([𝐴 / 𝑥]∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑦 ∈ 𝐵 [𝐴 / 𝑥]𝜑)) |
29 | 19, 28 | pm2.61ian 831 |
1
⊢
(Ⅎ𝑦𝐴 → ([𝐴 / 𝑥]∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑦 ∈ 𝐵 [𝐴 / 𝑥]𝜑)) |