Step |
Hyp |
Ref |
Expression |
1 |
|
s1val |
⊢ ( 𝑆 ∈ 𝐴 → ⟨“ 𝑆 ”⟩ = { ⟨ 0 , 𝑆 ⟩ } ) |
2 |
|
s1val |
⊢ ( 𝑇 ∈ 𝐴 → ⟨“ 𝑇 ”⟩ = { ⟨ 0 , 𝑇 ⟩ } ) |
3 |
1 2
|
eqeqan12d |
⊢ ( ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) → ( ⟨“ 𝑆 ”⟩ = ⟨“ 𝑇 ”⟩ ↔ { ⟨ 0 , 𝑆 ⟩ } = { ⟨ 0 , 𝑇 ⟩ } ) ) |
4 |
|
opex |
⊢ ⟨ 0 , 𝑆 ⟩ ∈ V |
5 |
|
sneqbg |
⊢ ( ⟨ 0 , 𝑆 ⟩ ∈ V → ( { ⟨ 0 , 𝑆 ⟩ } = { ⟨ 0 , 𝑇 ⟩ } ↔ ⟨ 0 , 𝑆 ⟩ = ⟨ 0 , 𝑇 ⟩ ) ) |
6 |
4 5
|
mp1i |
⊢ ( ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) → ( { ⟨ 0 , 𝑆 ⟩ } = { ⟨ 0 , 𝑇 ⟩ } ↔ ⟨ 0 , 𝑆 ⟩ = ⟨ 0 , 𝑇 ⟩ ) ) |
7 |
|
0z |
⊢ 0 ∈ ℤ |
8 |
|
eqid |
⊢ 0 = 0 |
9 |
|
opthg |
⊢ ( ( 0 ∈ ℤ ∧ 𝑆 ∈ 𝐴 ) → ( ⟨ 0 , 𝑆 ⟩ = ⟨ 0 , 𝑇 ⟩ ↔ ( 0 = 0 ∧ 𝑆 = 𝑇 ) ) ) |
10 |
9
|
baibd |
⊢ ( ( ( 0 ∈ ℤ ∧ 𝑆 ∈ 𝐴 ) ∧ 0 = 0 ) → ( ⟨ 0 , 𝑆 ⟩ = ⟨ 0 , 𝑇 ⟩ ↔ 𝑆 = 𝑇 ) ) |
11 |
8 10
|
mpan2 |
⊢ ( ( 0 ∈ ℤ ∧ 𝑆 ∈ 𝐴 ) → ( ⟨ 0 , 𝑆 ⟩ = ⟨ 0 , 𝑇 ⟩ ↔ 𝑆 = 𝑇 ) ) |
12 |
7 11
|
mpan |
⊢ ( 𝑆 ∈ 𝐴 → ( ⟨ 0 , 𝑆 ⟩ = ⟨ 0 , 𝑇 ⟩ ↔ 𝑆 = 𝑇 ) ) |
13 |
12
|
adantr |
⊢ ( ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) → ( ⟨ 0 , 𝑆 ⟩ = ⟨ 0 , 𝑇 ⟩ ↔ 𝑆 = 𝑇 ) ) |
14 |
3 6 13
|
3bitrd |
⊢ ( ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) → ( ⟨“ 𝑆 ”⟩ = ⟨“ 𝑇 ”⟩ ↔ 𝑆 = 𝑇 ) ) |