Proof of Theorem sbcrext
Step | Hyp | Ref
| Expression |
1 | | elex 2867 |
. 2
⊢ (A ∈ V → A ∈ V) |
2 | | sbcng 3086 |
. . . . 5
⊢ (A ∈ V →
([̣A / x]̣ ¬ ∀y ∈ B ¬ φ ↔ ¬ [̣A / x]̣∀y ∈ B ¬ φ)) |
3 | 2 | adantr 451 |
. . . 4
⊢ ((A ∈ V ∧ ℲyA) →
([̣A / x]̣ ¬ ∀y ∈ B ¬ φ ↔ ¬ [̣A / x]̣∀y ∈ B ¬ φ)) |
4 | | sbcralt 3118 |
. . . . . 6
⊢ ((A ∈ V ∧ ℲyA) →
([̣A / x]̣∀y ∈ B ¬ φ ↔ ∀y ∈ B
[̣A / x]̣ ¬ φ)) |
5 | | nfnfc1 2492 |
. . . . . . . . 9
⊢ ℲyℲyA |
6 | | id 19 |
. . . . . . . . . 10
⊢
(ℲyA → ℲyA) |
7 | | nfcvd 2490 |
. . . . . . . . . 10
⊢
(ℲyA → ℲyV) |
8 | 6, 7 | nfeld 2504 |
. . . . . . . . 9
⊢
(ℲyA → Ⅎy A ∈ V) |
9 | 5, 8 | nfan1 1881 |
. . . . . . . 8
⊢ Ⅎy(ℲyA ∧ A ∈ V) |
10 | | sbcng 3086 |
. . . . . . . . 9
⊢ (A ∈ V →
([̣A / x]̣ ¬ φ ↔ ¬ [̣A / x]̣φ)) |
11 | 10 | adantl 452 |
. . . . . . . 8
⊢
((ℲyA ∧ A ∈ V) →
([̣A / x]̣ ¬ φ ↔ ¬ [̣A / x]̣φ)) |
12 | 9, 11 | ralbid 2632 |
. . . . . . 7
⊢
((ℲyA ∧ A ∈ V) →
(∀y
∈ B
[̣A / x]̣ ¬ φ ↔ ∀y ∈ B ¬
[̣A / x]̣φ)) |
13 | 12 | ancoms 439 |
. . . . . 6
⊢ ((A ∈ V ∧ ℲyA) →
(∀y
∈ B
[̣A / x]̣ ¬ φ ↔ ∀y ∈ B ¬
[̣A / x]̣φ)) |
14 | 4, 13 | bitrd 244 |
. . . . 5
⊢ ((A ∈ V ∧ ℲyA) →
([̣A / x]̣∀y ∈ B ¬ φ ↔ ∀y ∈ B ¬
[̣A / x]̣φ)) |
15 | 14 | notbid 285 |
. . . 4
⊢ ((A ∈ V ∧ ℲyA) →
(¬ [̣A / x]̣∀y ∈ B ¬ φ ↔ ¬ ∀y ∈ B ¬
[̣A / x]̣φ)) |
16 | 3, 15 | bitrd 244 |
. . 3
⊢ ((A ∈ V ∧ ℲyA) →
([̣A / x]̣ ¬ ∀y ∈ B ¬ φ ↔ ¬ ∀y ∈ B ¬
[̣A / x]̣φ)) |
17 | | dfrex2 2627 |
. . . 4
⊢ (∃y ∈ B φ ↔ ¬ ∀y ∈ B ¬ φ) |
18 | 17 | sbcbii 3101 |
. . 3
⊢ ([̣A / x]̣∃y ∈ B φ ↔
[̣A / x]̣ ¬ ∀y ∈ B ¬ φ) |
19 | | dfrex2 2627 |
. . 3
⊢ (∃y ∈ B
[̣A / x]̣φ
↔ ¬ ∀y ∈ B ¬ [̣A
/ x]̣φ) |
20 | 16, 18, 19 | 3bitr4g 279 |
. 2
⊢ ((A ∈ V ∧ ℲyA) →
([̣A / x]̣∃y ∈ B φ ↔
∃y ∈ B
[̣A / x]̣φ)) |
21 | 1, 20 | sylan 457 |
1
⊢ ((A ∈ V ∧
ℲyA) → ([̣A / x]̣∃y ∈ B φ ↔
∃y ∈ B
[̣A / x]̣φ)) |