Step | Hyp | Ref
| Expression |
1 | | idn2 38838 |
. . . . . . 7
⊢ ( 𝐴 ∈ 𝐵 , 𝑥 = 𝐴 ▶ 𝑥 = 𝐴 ) |
2 | | 3mix3 1232 |
. . . . . . . . . 10
⊢ (𝑥 = 𝐴 → (𝑥 = 𝐶 ∨ 𝑥 = 𝐷 ∨ 𝑥 = 𝐴)) |
3 | 1, 2 | e2 38856 |
. . . . . . . . 9
⊢ ( 𝐴 ∈ 𝐵 , 𝑥 = 𝐴 ▶ (𝑥 = 𝐶 ∨ 𝑥 = 𝐷 ∨ 𝑥 = 𝐴) ) |
4 | | abid 2610 |
. . . . . . . . 9
⊢ (𝑥 ∈ {𝑥 ∣ (𝑥 = 𝐶 ∨ 𝑥 = 𝐷 ∨ 𝑥 = 𝐴)} ↔ (𝑥 = 𝐶 ∨ 𝑥 = 𝐷 ∨ 𝑥 = 𝐴)) |
5 | 3, 4 | e2bir 38858 |
. . . . . . . 8
⊢ ( 𝐴 ∈ 𝐵 , 𝑥 = 𝐴 ▶ 𝑥 ∈ {𝑥 ∣ (𝑥 = 𝐶 ∨ 𝑥 = 𝐷 ∨ 𝑥 = 𝐴)} ) |
6 | | dftp2 4231 |
. . . . . . . . 9
⊢ {𝐶, 𝐷, 𝐴} = {𝑥 ∣ (𝑥 = 𝐶 ∨ 𝑥 = 𝐷 ∨ 𝑥 = 𝐴)} |
7 | 6 | eleq2i 2693 |
. . . . . . . 8
⊢ (𝑥 ∈ {𝐶, 𝐷, 𝐴} ↔ 𝑥 ∈ {𝑥 ∣ (𝑥 = 𝐶 ∨ 𝑥 = 𝐷 ∨ 𝑥 = 𝐴)}) |
8 | 5, 7 | e2bir 38858 |
. . . . . . 7
⊢ ( 𝐴 ∈ 𝐵 , 𝑥 = 𝐴 ▶ 𝑥 ∈ {𝐶, 𝐷, 𝐴} ) |
9 | | eleq1 2689 |
. . . . . . . 8
⊢ (𝑥 = 𝐴 → (𝑥 ∈ {𝐶, 𝐷, 𝐴} ↔ 𝐴 ∈ {𝐶, 𝐷, 𝐴})) |
10 | 9 | biimpd 219 |
. . . . . . 7
⊢ (𝑥 = 𝐴 → (𝑥 ∈ {𝐶, 𝐷, 𝐴} → 𝐴 ∈ {𝐶, 𝐷, 𝐴})) |
11 | 1, 8, 10 | e22 38896 |
. . . . . 6
⊢ ( 𝐴 ∈ 𝐵 , 𝑥 = 𝐴 ▶ 𝐴 ∈ {𝐶, 𝐷, 𝐴} ) |
12 | 11 | in2 38830 |
. . . . 5
⊢ ( 𝐴 ∈ 𝐵 ▶ (𝑥 = 𝐴 → 𝐴 ∈ {𝐶, 𝐷, 𝐴}) ) |
13 | 12 | gen11 38841 |
. . . 4
⊢ ( 𝐴 ∈ 𝐵 ▶ ∀𝑥(𝑥 = 𝐴 → 𝐴 ∈ {𝐶, 𝐷, 𝐴}) ) |
14 | | 19.23v 1902 |
. . . 4
⊢
(∀𝑥(𝑥 = 𝐴 → 𝐴 ∈ {𝐶, 𝐷, 𝐴}) ↔ (∃𝑥 𝑥 = 𝐴 → 𝐴 ∈ {𝐶, 𝐷, 𝐴})) |
15 | 13, 14 | e1bi 38854 |
. . 3
⊢ ( 𝐴 ∈ 𝐵 ▶ (∃𝑥 𝑥 = 𝐴 → 𝐴 ∈ {𝐶, 𝐷, 𝐴}) ) |
16 | | idn1 38790 |
. . . 4
⊢ ( 𝐴 ∈ 𝐵 ▶ 𝐴 ∈ 𝐵 ) |
17 | | elisset 3215 |
. . . 4
⊢ (𝐴 ∈ 𝐵 → ∃𝑥 𝑥 = 𝐴) |
18 | 16, 17 | e1a 38852 |
. . 3
⊢ ( 𝐴 ∈ 𝐵 ▶ ∃𝑥 𝑥 = 𝐴 ) |
19 | | id 22 |
. . 3
⊢
((∃𝑥 𝑥 = 𝐴 → 𝐴 ∈ {𝐶, 𝐷, 𝐴}) → (∃𝑥 𝑥 = 𝐴 → 𝐴 ∈ {𝐶, 𝐷, 𝐴})) |
20 | 15, 18, 19 | e11 38913 |
. 2
⊢ ( 𝐴 ∈ 𝐵 ▶ 𝐴 ∈ {𝐶, 𝐷, 𝐴} ) |
21 | 20 | in1 38787 |
1
⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ {𝐶, 𝐷, 𝐴}) |