Proof of Theorem oteqex
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | simp3 1138 | . . 3
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝐶 ∈ V) → 𝐶 ∈ V) | 
| 2 | 1 | a1i 11 | . 2
⊢
(〈〈𝐴,
𝐵〉, 𝐶〉 = 〈〈𝑅, 𝑆〉, 𝑇〉 → ((𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝐶 ∈ V) → 𝐶 ∈ V)) | 
| 3 |  | simp3 1138 | . . 3
⊢ ((𝑅 ∈ V ∧ 𝑆 ∈ V ∧ 𝑇 ∈ V) → 𝑇 ∈ V) | 
| 4 |  | oteqex2 5503 | . . 3
⊢
(〈〈𝐴,
𝐵〉, 𝐶〉 = 〈〈𝑅, 𝑆〉, 𝑇〉 → (𝐶 ∈ V ↔ 𝑇 ∈ V)) | 
| 5 | 3, 4 | imbitrrid 246 | . 2
⊢
(〈〈𝐴,
𝐵〉, 𝐶〉 = 〈〈𝑅, 𝑆〉, 𝑇〉 → ((𝑅 ∈ V ∧ 𝑆 ∈ V ∧ 𝑇 ∈ V) → 𝐶 ∈ V)) | 
| 6 |  | opex 5468 | . . . . . . . 8
⊢
〈𝐴, 𝐵〉 ∈ V | 
| 7 |  | opthg 5481 | . . . . . . . 8
⊢
((〈𝐴, 𝐵〉 ∈ V ∧ 𝐶 ∈ V) →
(〈〈𝐴, 𝐵〉, 𝐶〉 = 〈〈𝑅, 𝑆〉, 𝑇〉 ↔ (〈𝐴, 𝐵〉 = 〈𝑅, 𝑆〉 ∧ 𝐶 = 𝑇))) | 
| 8 | 6, 7 | mpan 690 | . . . . . . 7
⊢ (𝐶 ∈ V →
(〈〈𝐴, 𝐵〉, 𝐶〉 = 〈〈𝑅, 𝑆〉, 𝑇〉 ↔ (〈𝐴, 𝐵〉 = 〈𝑅, 𝑆〉 ∧ 𝐶 = 𝑇))) | 
| 9 | 8 | simprbda 498 | . . . . . 6
⊢ ((𝐶 ∈ V ∧
〈〈𝐴, 𝐵〉, 𝐶〉 = 〈〈𝑅, 𝑆〉, 𝑇〉) → 〈𝐴, 𝐵〉 = 〈𝑅, 𝑆〉) | 
| 10 |  | opeqex 5502 | . . . . . 6
⊢
(〈𝐴, 𝐵〉 = 〈𝑅, 𝑆〉 → ((𝐴 ∈ V ∧ 𝐵 ∈ V) ↔ (𝑅 ∈ V ∧ 𝑆 ∈ V))) | 
| 11 | 9, 10 | syl 17 | . . . . 5
⊢ ((𝐶 ∈ V ∧
〈〈𝐴, 𝐵〉, 𝐶〉 = 〈〈𝑅, 𝑆〉, 𝑇〉) → ((𝐴 ∈ V ∧ 𝐵 ∈ V) ↔ (𝑅 ∈ V ∧ 𝑆 ∈ V))) | 
| 12 | 4 | adantl 481 | . . . . 5
⊢ ((𝐶 ∈ V ∧
〈〈𝐴, 𝐵〉, 𝐶〉 = 〈〈𝑅, 𝑆〉, 𝑇〉) → (𝐶 ∈ V ↔ 𝑇 ∈ V)) | 
| 13 | 11, 12 | anbi12d 632 | . . . 4
⊢ ((𝐶 ∈ V ∧
〈〈𝐴, 𝐵〉, 𝐶〉 = 〈〈𝑅, 𝑆〉, 𝑇〉) → (((𝐴 ∈ V ∧ 𝐵 ∈ V) ∧ 𝐶 ∈ V) ↔ ((𝑅 ∈ V ∧ 𝑆 ∈ V) ∧ 𝑇 ∈ V))) | 
| 14 |  | df-3an 1088 | . . . 4
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝐶 ∈ V) ↔ ((𝐴 ∈ V ∧ 𝐵 ∈ V) ∧ 𝐶 ∈ V)) | 
| 15 |  | df-3an 1088 | . . . 4
⊢ ((𝑅 ∈ V ∧ 𝑆 ∈ V ∧ 𝑇 ∈ V) ↔ ((𝑅 ∈ V ∧ 𝑆 ∈ V) ∧ 𝑇 ∈ V)) | 
| 16 | 13, 14, 15 | 3bitr4g 314 | . . 3
⊢ ((𝐶 ∈ V ∧
〈〈𝐴, 𝐵〉, 𝐶〉 = 〈〈𝑅, 𝑆〉, 𝑇〉) → ((𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝐶 ∈ V) ↔ (𝑅 ∈ V ∧ 𝑆 ∈ V ∧ 𝑇 ∈ V))) | 
| 17 | 16 | expcom 413 | . 2
⊢
(〈〈𝐴,
𝐵〉, 𝐶〉 = 〈〈𝑅, 𝑆〉, 𝑇〉 → (𝐶 ∈ V → ((𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝐶 ∈ V) ↔ (𝑅 ∈ V ∧ 𝑆 ∈ V ∧ 𝑇 ∈ V)))) | 
| 18 | 2, 5, 17 | pm5.21ndd 379 | 1
⊢
(〈〈𝐴,
𝐵〉, 𝐶〉 = 〈〈𝑅, 𝑆〉, 𝑇〉 → ((𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝐶 ∈ V) ↔ (𝑅 ∈ V ∧ 𝑆 ∈ V ∧ 𝑇 ∈ V))) |