Step | Hyp | Ref
| Expression |
1 | | idn1 43637 |
. . . . . . 7
⊢ ( (𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴) ▶ (𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴) ) |
2 | | simp3 1136 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴) → 𝐶 ∈ 𝐴) |
3 | 1, 2 | e1a 43690 |
. . . . . 6
⊢ ( (𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴) ▶ 𝐶 ∈ 𝐴 ) |
4 | | tpid3g 4775 |
. . . . . 6
⊢ (𝐶 ∈ 𝐴 → 𝐶 ∈ {𝐴, 𝐵, 𝐶}) |
5 | 3, 4 | e1a 43690 |
. . . . 5
⊢ ( (𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴) ▶ 𝐶 ∈ {𝐴, 𝐵, 𝐶} ) |
6 | | idn2 43676 |
. . . . . 6
⊢ ( (𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴) , 𝑥 = 𝐴 ▶ 𝑥 = 𝐴 ) |
7 | | eleq2 2820 |
. . . . . . 7
⊢ (𝑥 = 𝐴 → (𝐶 ∈ 𝑥 ↔ 𝐶 ∈ 𝐴)) |
8 | 7 | biimprd 247 |
. . . . . 6
⊢ (𝑥 = 𝐴 → (𝐶 ∈ 𝐴 → 𝐶 ∈ 𝑥)) |
9 | 6, 3, 8 | e21 43793 |
. . . . 5
⊢ ( (𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴) , 𝑥 = 𝐴 ▶ 𝐶 ∈ 𝑥 ) |
10 | | pm3.2 468 |
. . . . 5
⊢ (𝐶 ∈ {𝐴, 𝐵, 𝐶} → (𝐶 ∈ 𝑥 → (𝐶 ∈ {𝐴, 𝐵, 𝐶} ∧ 𝐶 ∈ 𝑥))) |
11 | 5, 9, 10 | e12 43787 |
. . . 4
⊢ ( (𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴) , 𝑥 = 𝐴 ▶ (𝐶 ∈ {𝐴, 𝐵, 𝐶} ∧ 𝐶 ∈ 𝑥) ) |
12 | | elex22 3495 |
. . . 4
⊢ ((𝐶 ∈ {𝐴, 𝐵, 𝐶} ∧ 𝐶 ∈ 𝑥) → ∃𝑦(𝑦 ∈ {𝐴, 𝐵, 𝐶} ∧ 𝑦 ∈ 𝑥)) |
13 | 11, 12 | e2 43694 |
. . 3
⊢ ( (𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴) , 𝑥 = 𝐴 ▶ ∃𝑦(𝑦 ∈ {𝐴, 𝐵, 𝐶} ∧ 𝑦 ∈ 𝑥) ) |
14 | 13 | in2 43668 |
. 2
⊢ ( (𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴) ▶ (𝑥 = 𝐴 → ∃𝑦(𝑦 ∈ {𝐴, 𝐵, 𝐶} ∧ 𝑦 ∈ 𝑥)) ) |
15 | 14 | in1 43634 |
1
⊢ ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴) → (𝑥 = 𝐴 → ∃𝑦(𝑦 ∈ {𝐴, 𝐵, 𝐶} ∧ 𝑦 ∈ 𝑥))) |