Step | Hyp | Ref
| Expression |
1 | | df-rab 3431 |
. . 3
⊢ {𝑥 ∈ 𝐵 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐵 ∧ 𝜑)} |
2 | 1 | eleq2i 2823 |
. 2
⊢ (𝐴 ∈ {𝑥 ∈ 𝐵 ∣ 𝜑} ↔ 𝐴 ∈ {𝑥 ∣ (𝑥 ∈ 𝐵 ∧ 𝜑)}) |
3 | | id 22 |
. . 3
⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ 𝐵) |
4 | | nfa1 2146 |
. . . . 5
⊢
Ⅎ𝑥∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) |
5 | | nfv 1915 |
. . . . 5
⊢
Ⅎ𝑥 𝐴 ∈ 𝐵 |
6 | 4, 5 | nfan 1900 |
. . . 4
⊢
Ⅎ𝑥(∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ 𝐴 ∈ 𝐵) |
7 | | sp 2174 |
. . . . . 6
⊢
(∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) → (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))) |
8 | | eleq1 2819 |
. . . . . . . . . 10
⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵)) |
9 | 8 | biimparc 478 |
. . . . . . . . 9
⊢ ((𝐴 ∈ 𝐵 ∧ 𝑥 = 𝐴) → 𝑥 ∈ 𝐵) |
10 | 9 | biantrurd 531 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝐵 ∧ 𝑥 = 𝐴) → (𝜑 ↔ (𝑥 ∈ 𝐵 ∧ 𝜑))) |
11 | 10 | bibi1d 342 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝐵 ∧ 𝑥 = 𝐴) → ((𝜑 ↔ 𝜓) ↔ ((𝑥 ∈ 𝐵 ∧ 𝜑) ↔ 𝜓))) |
12 | 11 | pm5.74da 800 |
. . . . . 6
⊢ (𝐴 ∈ 𝐵 → ((𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ↔ (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 ∧ 𝜑) ↔ 𝜓)))) |
13 | 7, 12 | syl5ibcom 244 |
. . . . 5
⊢
(∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) → (𝐴 ∈ 𝐵 → (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 ∧ 𝜑) ↔ 𝜓)))) |
14 | 13 | imp 405 |
. . . 4
⊢
((∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ 𝐴 ∈ 𝐵) → (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 ∧ 𝜑) ↔ 𝜓))) |
15 | 6, 14 | alrimi 2204 |
. . 3
⊢
((∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ 𝐴 ∈ 𝐵) → ∀𝑥(𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 ∧ 𝜑) ↔ 𝜓))) |
16 | | elabgt 3661 |
. . 3
⊢ ((𝐴 ∈ 𝐵 ∧ ∀𝑥(𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 ∧ 𝜑) ↔ 𝜓))) → (𝐴 ∈ {𝑥 ∣ (𝑥 ∈ 𝐵 ∧ 𝜑)} ↔ 𝜓)) |
17 | 3, 15, 16 | syl2an2 682 |
. 2
⊢
((∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ 𝐴 ∈ 𝐵) → (𝐴 ∈ {𝑥 ∣ (𝑥 ∈ 𝐵 ∧ 𝜑)} ↔ 𝜓)) |
18 | 2, 17 | bitrid 282 |
1
⊢
((∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ 𝐴 ∈ 𝐵) → (𝐴 ∈ {𝑥 ∈ 𝐵 ∣ 𝜑} ↔ 𝜓)) |