Step |
Hyp |
Ref |
Expression |
1 |
|
brtp.1 |
⊢ 𝑋 ∈ V |
2 |
|
brtp.2 |
⊢ 𝑌 ∈ V |
3 |
|
df-br |
⊢ ( 𝑋 { 〈 𝐴 , 𝐵 〉 , 〈 𝐶 , 𝐷 〉 , 〈 𝐸 , 𝐹 〉 } 𝑌 ↔ 〈 𝑋 , 𝑌 〉 ∈ { 〈 𝐴 , 𝐵 〉 , 〈 𝐶 , 𝐷 〉 , 〈 𝐸 , 𝐹 〉 } ) |
4 |
|
opex |
⊢ 〈 𝑋 , 𝑌 〉 ∈ V |
5 |
4
|
eltp |
⊢ ( 〈 𝑋 , 𝑌 〉 ∈ { 〈 𝐴 , 𝐵 〉 , 〈 𝐶 , 𝐷 〉 , 〈 𝐸 , 𝐹 〉 } ↔ ( 〈 𝑋 , 𝑌 〉 = 〈 𝐴 , 𝐵 〉 ∨ 〈 𝑋 , 𝑌 〉 = 〈 𝐶 , 𝐷 〉 ∨ 〈 𝑋 , 𝑌 〉 = 〈 𝐸 , 𝐹 〉 ) ) |
6 |
1 2
|
opth |
⊢ ( 〈 𝑋 , 𝑌 〉 = 〈 𝐴 , 𝐵 〉 ↔ ( 𝑋 = 𝐴 ∧ 𝑌 = 𝐵 ) ) |
7 |
1 2
|
opth |
⊢ ( 〈 𝑋 , 𝑌 〉 = 〈 𝐶 , 𝐷 〉 ↔ ( 𝑋 = 𝐶 ∧ 𝑌 = 𝐷 ) ) |
8 |
1 2
|
opth |
⊢ ( 〈 𝑋 , 𝑌 〉 = 〈 𝐸 , 𝐹 〉 ↔ ( 𝑋 = 𝐸 ∧ 𝑌 = 𝐹 ) ) |
9 |
6 7 8
|
3orbi123i |
⊢ ( ( 〈 𝑋 , 𝑌 〉 = 〈 𝐴 , 𝐵 〉 ∨ 〈 𝑋 , 𝑌 〉 = 〈 𝐶 , 𝐷 〉 ∨ 〈 𝑋 , 𝑌 〉 = 〈 𝐸 , 𝐹 〉 ) ↔ ( ( 𝑋 = 𝐴 ∧ 𝑌 = 𝐵 ) ∨ ( 𝑋 = 𝐶 ∧ 𝑌 = 𝐷 ) ∨ ( 𝑋 = 𝐸 ∧ 𝑌 = 𝐹 ) ) ) |
10 |
3 5 9
|
3bitri |
⊢ ( 𝑋 { 〈 𝐴 , 𝐵 〉 , 〈 𝐶 , 𝐷 〉 , 〈 𝐸 , 𝐹 〉 } 𝑌 ↔ ( ( 𝑋 = 𝐴 ∧ 𝑌 = 𝐵 ) ∨ ( 𝑋 = 𝐶 ∧ 𝑌 = 𝐷 ) ∨ ( 𝑋 = 𝐸 ∧ 𝑌 = 𝐹 ) ) ) |