Step | Hyp | Ref
| Expression |
1 | | elxp 5657 |
. 2
⊢ (𝐴 ∈ (𝐵 × 𝐶) ↔ ∃𝑏∃𝑐(𝐴 = ⟨𝑏, 𝑐⟩ ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶))) |
2 | | vex 3450 |
. . . . . . 7
⊢ 𝑏 ∈ V |
3 | | vex 3450 |
. . . . . . 7
⊢ 𝑐 ∈ V |
4 | 2, 3 | op2ndd 7933 |
. . . . . 6
⊢ (𝐴 = ⟨𝑏, 𝑐⟩ → (2nd ‘𝐴) = 𝑐) |
5 | 4 | eleq1d 2823 |
. . . . 5
⊢ (𝐴 = ⟨𝑏, 𝑐⟩ → ((2nd ‘𝐴) ∈ 𝐶 ↔ 𝑐 ∈ 𝐶)) |
6 | 5 | biimpar 479 |
. . . 4
⊢ ((𝐴 = ⟨𝑏, 𝑐⟩ ∧ 𝑐 ∈ 𝐶) → (2nd ‘𝐴) ∈ 𝐶) |
7 | 6 | adantrl 715 |
. . 3
⊢ ((𝐴 = ⟨𝑏, 𝑐⟩ ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (2nd ‘𝐴) ∈ 𝐶) |
8 | 7 | exlimivv 1936 |
. 2
⊢
(∃𝑏∃𝑐(𝐴 = ⟨𝑏, 𝑐⟩ ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (2nd ‘𝐴) ∈ 𝐶) |
9 | 1, 8 | sylbi 216 |
1
⊢ (𝐴 ∈ (𝐵 × 𝐶) → (2nd ‘𝐴) ∈ 𝐶) |