Step | Hyp | Ref
| Expression |
1 | | idn2 43306 |
. . . . . . 7
⊢ ( 𝐴 ∈ 𝐵 , 𝑥 = 𝐴 ▶ 𝑥 = 𝐴 ) |
2 | | 3mix3 1333 |
. . . . . . . . . 10
⊢ (𝑥 = 𝐴 → (𝑥 = 𝐶 ∨ 𝑥 = 𝐷 ∨ 𝑥 = 𝐴)) |
3 | 1, 2 | e2 43324 |
. . . . . . . . 9
⊢ ( 𝐴 ∈ 𝐵 , 𝑥 = 𝐴 ▶ (𝑥 = 𝐶 ∨ 𝑥 = 𝐷 ∨ 𝑥 = 𝐴) ) |
4 | | abid 2714 |
. . . . . . . . 9
⊢ (𝑥 ∈ {𝑥 ∣ (𝑥 = 𝐶 ∨ 𝑥 = 𝐷 ∨ 𝑥 = 𝐴)} ↔ (𝑥 = 𝐶 ∨ 𝑥 = 𝐷 ∨ 𝑥 = 𝐴)) |
5 | 3, 4 | e2bir 43326 |
. . . . . . . 8
⊢ ( 𝐴 ∈ 𝐵 , 𝑥 = 𝐴 ▶ 𝑥 ∈ {𝑥 ∣ (𝑥 = 𝐶 ∨ 𝑥 = 𝐷 ∨ 𝑥 = 𝐴)} ) |
6 | | dftp2 4691 |
. . . . . . . . 9
⊢ {𝐶, 𝐷, 𝐴} = {𝑥 ∣ (𝑥 = 𝐶 ∨ 𝑥 = 𝐷 ∨ 𝑥 = 𝐴)} |
7 | 6 | eleq2i 2826 |
. . . . . . . 8
⊢ (𝑥 ∈ {𝐶, 𝐷, 𝐴} ↔ 𝑥 ∈ {𝑥 ∣ (𝑥 = 𝐶 ∨ 𝑥 = 𝐷 ∨ 𝑥 = 𝐴)}) |
8 | 5, 7 | e2bir 43326 |
. . . . . . 7
⊢ ( 𝐴 ∈ 𝐵 , 𝑥 = 𝐴 ▶ 𝑥 ∈ {𝐶, 𝐷, 𝐴} ) |
9 | | eleq1 2822 |
. . . . . . . 8
⊢ (𝑥 = 𝐴 → (𝑥 ∈ {𝐶, 𝐷, 𝐴} ↔ 𝐴 ∈ {𝐶, 𝐷, 𝐴})) |
10 | 9 | biimpd 228 |
. . . . . . 7
⊢ (𝑥 = 𝐴 → (𝑥 ∈ {𝐶, 𝐷, 𝐴} → 𝐴 ∈ {𝐶, 𝐷, 𝐴})) |
11 | 1, 8, 10 | e22 43364 |
. . . . . 6
⊢ ( 𝐴 ∈ 𝐵 , 𝑥 = 𝐴 ▶ 𝐴 ∈ {𝐶, 𝐷, 𝐴} ) |
12 | 11 | in2 43298 |
. . . . 5
⊢ ( 𝐴 ∈ 𝐵 ▶ (𝑥 = 𝐴 → 𝐴 ∈ {𝐶, 𝐷, 𝐴}) ) |
13 | 12 | gen11 43309 |
. . . 4
⊢ ( 𝐴 ∈ 𝐵 ▶ ∀𝑥(𝑥 = 𝐴 → 𝐴 ∈ {𝐶, 𝐷, 𝐴}) ) |
14 | | 19.23v 1946 |
. . . 4
⊢
(∀𝑥(𝑥 = 𝐴 → 𝐴 ∈ {𝐶, 𝐷, 𝐴}) ↔ (∃𝑥 𝑥 = 𝐴 → 𝐴 ∈ {𝐶, 𝐷, 𝐴})) |
15 | 13, 14 | e1bi 43322 |
. . 3
⊢ ( 𝐴 ∈ 𝐵 ▶ (∃𝑥 𝑥 = 𝐴 → 𝐴 ∈ {𝐶, 𝐷, 𝐴}) ) |
16 | | idn1 43267 |
. . . 4
⊢ ( 𝐴 ∈ 𝐵 ▶ 𝐴 ∈ 𝐵 ) |
17 | | elisset 2816 |
. . . 4
⊢ (𝐴 ∈ 𝐵 → ∃𝑥 𝑥 = 𝐴) |
18 | 16, 17 | e1a 43320 |
. . 3
⊢ ( 𝐴 ∈ 𝐵 ▶ ∃𝑥 𝑥 = 𝐴 ) |
19 | | id 22 |
. . 3
⊢
((∃𝑥 𝑥 = 𝐴 → 𝐴 ∈ {𝐶, 𝐷, 𝐴}) → (∃𝑥 𝑥 = 𝐴 → 𝐴 ∈ {𝐶, 𝐷, 𝐴})) |
20 | 15, 18, 19 | e11 43381 |
. 2
⊢ ( 𝐴 ∈ 𝐵 ▶ 𝐴 ∈ {𝐶, 𝐷, 𝐴} ) |
21 | 20 | in1 43264 |
1
⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ {𝐶, 𝐷, 𝐴}) |