Step | Hyp | Ref
| Expression |
1 | | df-bj-gab 35130 |
. . 3
⊢ {𝐵 ∣ 𝑥 ∣ 𝜓} = {𝑦 ∣ ∃𝑥(𝐵 = 𝑦 ∧ 𝜓)} |
2 | 1 | eleq2i 2830 |
. 2
⊢ (𝐴 ∈ {𝐵 ∣ 𝑥 ∣ 𝜓} ↔ 𝐴 ∈ {𝑦 ∣ ∃𝑥(𝐵 = 𝑦 ∧ 𝜓)}) |
3 | | bj-elgab.ex |
. . . 4
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
4 | | bj-elgab.nf |
. . . . . . . . 9
⊢ (𝜑 → ∀𝑥𝜑) |
5 | 4 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 = 𝐴) → ∀𝑥𝜑) |
6 | | bj-elgab.nfa |
. . . . . . . . . 10
⊢ (𝜑 → Ⅎ𝑥𝐴) |
7 | | nfcvd 2908 |
. . . . . . . . . . . 12
⊢
(Ⅎ𝑥𝐴 → Ⅎ𝑥𝑦) |
8 | | id 22 |
. . . . . . . . . . . 12
⊢
(Ⅎ𝑥𝐴 → Ⅎ𝑥𝐴) |
9 | 7, 8 | nfeqd 2917 |
. . . . . . . . . . 11
⊢
(Ⅎ𝑥𝐴 → Ⅎ𝑥 𝑦 = 𝐴) |
10 | 9 | nf5rd 2189 |
. . . . . . . . . 10
⊢
(Ⅎ𝑥𝐴 → (𝑦 = 𝐴 → ∀𝑥 𝑦 = 𝐴)) |
11 | 6, 10 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (𝑦 = 𝐴 → ∀𝑥 𝑦 = 𝐴)) |
12 | 11 | imp 407 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 = 𝐴) → ∀𝑥 𝑦 = 𝐴) |
13 | | 19.26 1873 |
. . . . . . . 8
⊢
(∀𝑥(𝜑 ∧ 𝑦 = 𝐴) ↔ (∀𝑥𝜑 ∧ ∀𝑥 𝑦 = 𝐴)) |
14 | 5, 12, 13 | sylanbrc 583 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 = 𝐴) → ∀𝑥(𝜑 ∧ 𝑦 = 𝐴)) |
15 | | eqeq2 2750 |
. . . . . . . . . 10
⊢ (𝑦 = 𝐴 → (𝐵 = 𝑦 ↔ 𝐵 = 𝐴)) |
16 | | eqcom 2745 |
. . . . . . . . . 10
⊢ (𝐵 = 𝐴 ↔ 𝐴 = 𝐵) |
17 | 15, 16 | bitrdi 287 |
. . . . . . . . 9
⊢ (𝑦 = 𝐴 → (𝐵 = 𝑦 ↔ 𝐴 = 𝐵)) |
18 | 17 | anbi1d 630 |
. . . . . . . 8
⊢ (𝑦 = 𝐴 → ((𝐵 = 𝑦 ∧ 𝜓) ↔ (𝐴 = 𝐵 ∧ 𝜓))) |
19 | 18 | adantl 482 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 = 𝐴) → ((𝐵 = 𝑦 ∧ 𝜓) ↔ (𝐴 = 𝐵 ∧ 𝜓))) |
20 | 14, 19 | exbidh 1870 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 = 𝐴) → (∃𝑥(𝐵 = 𝑦 ∧ 𝜓) ↔ ∃𝑥(𝐴 = 𝐵 ∧ 𝜓))) |
21 | 20 | ex 413 |
. . . . 5
⊢ (𝜑 → (𝑦 = 𝐴 → (∃𝑥(𝐵 = 𝑦 ∧ 𝜓) ↔ ∃𝑥(𝐴 = 𝐵 ∧ 𝜓)))) |
22 | 21 | alrimiv 1930 |
. . . 4
⊢ (𝜑 → ∀𝑦(𝑦 = 𝐴 → (∃𝑥(𝐵 = 𝑦 ∧ 𝜓) ↔ ∃𝑥(𝐴 = 𝐵 ∧ 𝜓)))) |
23 | | elabgt 3602 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑦(𝑦 = 𝐴 → (∃𝑥(𝐵 = 𝑦 ∧ 𝜓) ↔ ∃𝑥(𝐴 = 𝐵 ∧ 𝜓)))) → (𝐴 ∈ {𝑦 ∣ ∃𝑥(𝐵 = 𝑦 ∧ 𝜓)} ↔ ∃𝑥(𝐴 = 𝐵 ∧ 𝜓))) |
24 | 3, 22, 23 | syl2anc 584 |
. . 3
⊢ (𝜑 → (𝐴 ∈ {𝑦 ∣ ∃𝑥(𝐵 = 𝑦 ∧ 𝜓)} ↔ ∃𝑥(𝐴 = 𝐵 ∧ 𝜓))) |
25 | | bj-elgab.is |
. . 3
⊢ (𝜑 → (∃𝑥(𝐴 = 𝐵 ∧ 𝜓) ↔ 𝜒)) |
26 | 24, 25 | bitrd 278 |
. 2
⊢ (𝜑 → (𝐴 ∈ {𝑦 ∣ ∃𝑥(𝐵 = 𝑦 ∧ 𝜓)} ↔ 𝜒)) |
27 | 2, 26 | syl5bb 283 |
1
⊢ (𝜑 → (𝐴 ∈ {𝐵 ∣ 𝑥 ∣ 𝜓} ↔ 𝜒)) |