Step | Hyp | Ref
| Expression |
1 | | elex 3450 |
. . 3
⊢ (𝐵 ∈ 𝐹 → 𝐵 ∈ V) |
2 | 1 | a1i 11 |
. 2
⊢ (𝜑 → (𝐵 ∈ 𝐹 → 𝐵 ∈ V)) |
3 | | isfild.2 |
. . . 4
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
4 | | ssexg 5247 |
. . . . 5
⊢ ((𝐵 ⊆ 𝐴 ∧ 𝐴 ∈ 𝑉) → 𝐵 ∈ V) |
5 | 4 | expcom 414 |
. . . 4
⊢ (𝐴 ∈ 𝑉 → (𝐵 ⊆ 𝐴 → 𝐵 ∈ V)) |
6 | 3, 5 | syl 17 |
. . 3
⊢ (𝜑 → (𝐵 ⊆ 𝐴 → 𝐵 ∈ V)) |
7 | 6 | adantrd 492 |
. 2
⊢ (𝜑 → ((𝐵 ⊆ 𝐴 ∧ [𝐵 / 𝑥]𝜓) → 𝐵 ∈ V)) |
8 | | eleq1 2826 |
. . . . . 6
⊢ (𝑦 = 𝐵 → (𝑦 ∈ 𝐹 ↔ 𝐵 ∈ 𝐹)) |
9 | | sseq1 3946 |
. . . . . . 7
⊢ (𝑦 = 𝐵 → (𝑦 ⊆ 𝐴 ↔ 𝐵 ⊆ 𝐴)) |
10 | | dfsbcq 3718 |
. . . . . . 7
⊢ (𝑦 = 𝐵 → ([𝑦 / 𝑥]𝜓 ↔ [𝐵 / 𝑥]𝜓)) |
11 | 9, 10 | anbi12d 631 |
. . . . . 6
⊢ (𝑦 = 𝐵 → ((𝑦 ⊆ 𝐴 ∧ [𝑦 / 𝑥]𝜓) ↔ (𝐵 ⊆ 𝐴 ∧ [𝐵 / 𝑥]𝜓))) |
12 | 8, 11 | bibi12d 346 |
. . . . 5
⊢ (𝑦 = 𝐵 → ((𝑦 ∈ 𝐹 ↔ (𝑦 ⊆ 𝐴 ∧ [𝑦 / 𝑥]𝜓)) ↔ (𝐵 ∈ 𝐹 ↔ (𝐵 ⊆ 𝐴 ∧ [𝐵 / 𝑥]𝜓)))) |
13 | 12 | imbi2d 341 |
. . . 4
⊢ (𝑦 = 𝐵 → ((𝜑 → (𝑦 ∈ 𝐹 ↔ (𝑦 ⊆ 𝐴 ∧ [𝑦 / 𝑥]𝜓))) ↔ (𝜑 → (𝐵 ∈ 𝐹 ↔ (𝐵 ⊆ 𝐴 ∧ [𝐵 / 𝑥]𝜓))))) |
14 | | nfv 1917 |
. . . . . 6
⊢
Ⅎ𝑥𝜑 |
15 | | nfv 1917 |
. . . . . . 7
⊢
Ⅎ𝑥 𝑦 ∈ 𝐹 |
16 | | nfv 1917 |
. . . . . . . 8
⊢
Ⅎ𝑥 𝑦 ⊆ 𝐴 |
17 | | nfsbc1v 3736 |
. . . . . . . 8
⊢
Ⅎ𝑥[𝑦 / 𝑥]𝜓 |
18 | 16, 17 | nfan 1902 |
. . . . . . 7
⊢
Ⅎ𝑥(𝑦 ⊆ 𝐴 ∧ [𝑦 / 𝑥]𝜓) |
19 | 15, 18 | nfbi 1906 |
. . . . . 6
⊢
Ⅎ𝑥(𝑦 ∈ 𝐹 ↔ (𝑦 ⊆ 𝐴 ∧ [𝑦 / 𝑥]𝜓)) |
20 | 14, 19 | nfim 1899 |
. . . . 5
⊢
Ⅎ𝑥(𝜑 → (𝑦 ∈ 𝐹 ↔ (𝑦 ⊆ 𝐴 ∧ [𝑦 / 𝑥]𝜓))) |
21 | | eleq1 2826 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐹 ↔ 𝑦 ∈ 𝐹)) |
22 | | sseq1 3946 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → (𝑥 ⊆ 𝐴 ↔ 𝑦 ⊆ 𝐴)) |
23 | | sbceq1a 3727 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → (𝜓 ↔ [𝑦 / 𝑥]𝜓)) |
24 | 22, 23 | anbi12d 631 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → ((𝑥 ⊆ 𝐴 ∧ 𝜓) ↔ (𝑦 ⊆ 𝐴 ∧ [𝑦 / 𝑥]𝜓))) |
25 | 21, 24 | bibi12d 346 |
. . . . . 6
⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐹 ↔ (𝑥 ⊆ 𝐴 ∧ 𝜓)) ↔ (𝑦 ∈ 𝐹 ↔ (𝑦 ⊆ 𝐴 ∧ [𝑦 / 𝑥]𝜓)))) |
26 | 25 | imbi2d 341 |
. . . . 5
⊢ (𝑥 = 𝑦 → ((𝜑 → (𝑥 ∈ 𝐹 ↔ (𝑥 ⊆ 𝐴 ∧ 𝜓))) ↔ (𝜑 → (𝑦 ∈ 𝐹 ↔ (𝑦 ⊆ 𝐴 ∧ [𝑦 / 𝑥]𝜓))))) |
27 | | isfild.1 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ 𝐹 ↔ (𝑥 ⊆ 𝐴 ∧ 𝜓))) |
28 | 20, 26, 27 | chvarfv 2233 |
. . . 4
⊢ (𝜑 → (𝑦 ∈ 𝐹 ↔ (𝑦 ⊆ 𝐴 ∧ [𝑦 / 𝑥]𝜓))) |
29 | 13, 28 | vtoclg 3505 |
. . 3
⊢ (𝐵 ∈ V → (𝜑 → (𝐵 ∈ 𝐹 ↔ (𝐵 ⊆ 𝐴 ∧ [𝐵 / 𝑥]𝜓)))) |
30 | 29 | com12 32 |
. 2
⊢ (𝜑 → (𝐵 ∈ V → (𝐵 ∈ 𝐹 ↔ (𝐵 ⊆ 𝐴 ∧ [𝐵 / 𝑥]𝜓)))) |
31 | 2, 7, 30 | pm5.21ndd 381 |
1
⊢ (𝜑 → (𝐵 ∈ 𝐹 ↔ (𝐵 ⊆ 𝐴 ∧ [𝐵 / 𝑥]𝜓))) |