| Step | Hyp | Ref
| Expression |
| 1 | | elex 3501 |
. . 3
⊢ (𝐵 ∈ 𝐹 → 𝐵 ∈ V) |
| 2 | 1 | a1i 11 |
. 2
⊢ (𝜑 → (𝐵 ∈ 𝐹 → 𝐵 ∈ V)) |
| 3 | | isfild.2 |
. . . 4
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
| 4 | | ssexg 5323 |
. . . . 5
⊢ ((𝐵 ⊆ 𝐴 ∧ 𝐴 ∈ 𝑉) → 𝐵 ∈ V) |
| 5 | 4 | expcom 413 |
. . . 4
⊢ (𝐴 ∈ 𝑉 → (𝐵 ⊆ 𝐴 → 𝐵 ∈ V)) |
| 6 | 3, 5 | syl 17 |
. . 3
⊢ (𝜑 → (𝐵 ⊆ 𝐴 → 𝐵 ∈ V)) |
| 7 | 6 | adantrd 491 |
. 2
⊢ (𝜑 → ((𝐵 ⊆ 𝐴 ∧ [𝐵 / 𝑥]𝜓) → 𝐵 ∈ V)) |
| 8 | | eleq1 2829 |
. . . . . 6
⊢ (𝑦 = 𝐵 → (𝑦 ∈ 𝐹 ↔ 𝐵 ∈ 𝐹)) |
| 9 | | sseq1 4009 |
. . . . . . 7
⊢ (𝑦 = 𝐵 → (𝑦 ⊆ 𝐴 ↔ 𝐵 ⊆ 𝐴)) |
| 10 | | dfsbcq 3790 |
. . . . . . 7
⊢ (𝑦 = 𝐵 → ([𝑦 / 𝑥]𝜓 ↔ [𝐵 / 𝑥]𝜓)) |
| 11 | 9, 10 | anbi12d 632 |
. . . . . 6
⊢ (𝑦 = 𝐵 → ((𝑦 ⊆ 𝐴 ∧ [𝑦 / 𝑥]𝜓) ↔ (𝐵 ⊆ 𝐴 ∧ [𝐵 / 𝑥]𝜓))) |
| 12 | 8, 11 | bibi12d 345 |
. . . . 5
⊢ (𝑦 = 𝐵 → ((𝑦 ∈ 𝐹 ↔ (𝑦 ⊆ 𝐴 ∧ [𝑦 / 𝑥]𝜓)) ↔ (𝐵 ∈ 𝐹 ↔ (𝐵 ⊆ 𝐴 ∧ [𝐵 / 𝑥]𝜓)))) |
| 13 | 12 | imbi2d 340 |
. . . 4
⊢ (𝑦 = 𝐵 → ((𝜑 → (𝑦 ∈ 𝐹 ↔ (𝑦 ⊆ 𝐴 ∧ [𝑦 / 𝑥]𝜓))) ↔ (𝜑 → (𝐵 ∈ 𝐹 ↔ (𝐵 ⊆ 𝐴 ∧ [𝐵 / 𝑥]𝜓))))) |
| 14 | | nfv 1914 |
. . . . . 6
⊢
Ⅎ𝑥𝜑 |
| 15 | | nfv 1914 |
. . . . . . 7
⊢
Ⅎ𝑥 𝑦 ∈ 𝐹 |
| 16 | | nfv 1914 |
. . . . . . . 8
⊢
Ⅎ𝑥 𝑦 ⊆ 𝐴 |
| 17 | | nfsbc1v 3808 |
. . . . . . . 8
⊢
Ⅎ𝑥[𝑦 / 𝑥]𝜓 |
| 18 | 16, 17 | nfan 1899 |
. . . . . . 7
⊢
Ⅎ𝑥(𝑦 ⊆ 𝐴 ∧ [𝑦 / 𝑥]𝜓) |
| 19 | 15, 18 | nfbi 1903 |
. . . . . 6
⊢
Ⅎ𝑥(𝑦 ∈ 𝐹 ↔ (𝑦 ⊆ 𝐴 ∧ [𝑦 / 𝑥]𝜓)) |
| 20 | 14, 19 | nfim 1896 |
. . . . 5
⊢
Ⅎ𝑥(𝜑 → (𝑦 ∈ 𝐹 ↔ (𝑦 ⊆ 𝐴 ∧ [𝑦 / 𝑥]𝜓))) |
| 21 | | eleq1 2829 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐹 ↔ 𝑦 ∈ 𝐹)) |
| 22 | | sseq1 4009 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → (𝑥 ⊆ 𝐴 ↔ 𝑦 ⊆ 𝐴)) |
| 23 | | sbceq1a 3799 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → (𝜓 ↔ [𝑦 / 𝑥]𝜓)) |
| 24 | 22, 23 | anbi12d 632 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → ((𝑥 ⊆ 𝐴 ∧ 𝜓) ↔ (𝑦 ⊆ 𝐴 ∧ [𝑦 / 𝑥]𝜓))) |
| 25 | 21, 24 | bibi12d 345 |
. . . . . 6
⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐹 ↔ (𝑥 ⊆ 𝐴 ∧ 𝜓)) ↔ (𝑦 ∈ 𝐹 ↔ (𝑦 ⊆ 𝐴 ∧ [𝑦 / 𝑥]𝜓)))) |
| 26 | 25 | imbi2d 340 |
. . . . 5
⊢ (𝑥 = 𝑦 → ((𝜑 → (𝑥 ∈ 𝐹 ↔ (𝑥 ⊆ 𝐴 ∧ 𝜓))) ↔ (𝜑 → (𝑦 ∈ 𝐹 ↔ (𝑦 ⊆ 𝐴 ∧ [𝑦 / 𝑥]𝜓))))) |
| 27 | | isfild.1 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ 𝐹 ↔ (𝑥 ⊆ 𝐴 ∧ 𝜓))) |
| 28 | 20, 26, 27 | chvarfv 2240 |
. . . 4
⊢ (𝜑 → (𝑦 ∈ 𝐹 ↔ (𝑦 ⊆ 𝐴 ∧ [𝑦 / 𝑥]𝜓))) |
| 29 | 13, 28 | vtoclg 3554 |
. . 3
⊢ (𝐵 ∈ V → (𝜑 → (𝐵 ∈ 𝐹 ↔ (𝐵 ⊆ 𝐴 ∧ [𝐵 / 𝑥]𝜓)))) |
| 30 | 29 | com12 32 |
. 2
⊢ (𝜑 → (𝐵 ∈ V → (𝐵 ∈ 𝐹 ↔ (𝐵 ⊆ 𝐴 ∧ [𝐵 / 𝑥]𝜓)))) |
| 31 | 2, 7, 30 | pm5.21ndd 379 |
1
⊢ (𝜑 → (𝐵 ∈ 𝐹 ↔ (𝐵 ⊆ 𝐴 ∧ [𝐵 / 𝑥]𝜓))) |