Proof of Theorem preq12b
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | preqr1.a | . . . . . 6
⊢ 𝐴 ∈ V | 
| 2 | 1 | prid1 4761 | . . . . 5
⊢ 𝐴 ∈ {𝐴, 𝐵} | 
| 3 |  | eleq2 2829 | . . . . 5
⊢ ({𝐴, 𝐵} = {𝐶, 𝐷} → (𝐴 ∈ {𝐴, 𝐵} ↔ 𝐴 ∈ {𝐶, 𝐷})) | 
| 4 | 2, 3 | mpbii 233 | . . . 4
⊢ ({𝐴, 𝐵} = {𝐶, 𝐷} → 𝐴 ∈ {𝐶, 𝐷}) | 
| 5 | 1 | elpr 4649 | . . . 4
⊢ (𝐴 ∈ {𝐶, 𝐷} ↔ (𝐴 = 𝐶 ∨ 𝐴 = 𝐷)) | 
| 6 | 4, 5 | sylib 218 | . . 3
⊢ ({𝐴, 𝐵} = {𝐶, 𝐷} → (𝐴 = 𝐶 ∨ 𝐴 = 𝐷)) | 
| 7 |  | preq1 4732 | . . . . . . . 8
⊢ (𝐴 = 𝐶 → {𝐴, 𝐵} = {𝐶, 𝐵}) | 
| 8 | 7 | eqeq1d 2738 | . . . . . . 7
⊢ (𝐴 = 𝐶 → ({𝐴, 𝐵} = {𝐶, 𝐷} ↔ {𝐶, 𝐵} = {𝐶, 𝐷})) | 
| 9 |  | preqr1.b | . . . . . . . 8
⊢ 𝐵 ∈ V | 
| 10 |  | preq12b.d | . . . . . . . 8
⊢ 𝐷 ∈ V | 
| 11 | 9, 10 | preqr2 4848 | . . . . . . 7
⊢ ({𝐶, 𝐵} = {𝐶, 𝐷} → 𝐵 = 𝐷) | 
| 12 | 8, 11 | biimtrdi 253 | . . . . . 6
⊢ (𝐴 = 𝐶 → ({𝐴, 𝐵} = {𝐶, 𝐷} → 𝐵 = 𝐷)) | 
| 13 | 12 | com12 32 | . . . . 5
⊢ ({𝐴, 𝐵} = {𝐶, 𝐷} → (𝐴 = 𝐶 → 𝐵 = 𝐷)) | 
| 14 | 13 | ancld 550 | . . . 4
⊢ ({𝐴, 𝐵} = {𝐶, 𝐷} → (𝐴 = 𝐶 → (𝐴 = 𝐶 ∧ 𝐵 = 𝐷))) | 
| 15 |  | prcom 4731 | . . . . . . 7
⊢ {𝐶, 𝐷} = {𝐷, 𝐶} | 
| 16 | 15 | eqeq2i 2749 | . . . . . 6
⊢ ({𝐴, 𝐵} = {𝐶, 𝐷} ↔ {𝐴, 𝐵} = {𝐷, 𝐶}) | 
| 17 |  | preq1 4732 | . . . . . . . . 9
⊢ (𝐴 = 𝐷 → {𝐴, 𝐵} = {𝐷, 𝐵}) | 
| 18 | 17 | eqeq1d 2738 | . . . . . . . 8
⊢ (𝐴 = 𝐷 → ({𝐴, 𝐵} = {𝐷, 𝐶} ↔ {𝐷, 𝐵} = {𝐷, 𝐶})) | 
| 19 |  | preq12b.c | . . . . . . . . 9
⊢ 𝐶 ∈ V | 
| 20 | 9, 19 | preqr2 4848 | . . . . . . . 8
⊢ ({𝐷, 𝐵} = {𝐷, 𝐶} → 𝐵 = 𝐶) | 
| 21 | 18, 20 | biimtrdi 253 | . . . . . . 7
⊢ (𝐴 = 𝐷 → ({𝐴, 𝐵} = {𝐷, 𝐶} → 𝐵 = 𝐶)) | 
| 22 | 21 | com12 32 | . . . . . 6
⊢ ({𝐴, 𝐵} = {𝐷, 𝐶} → (𝐴 = 𝐷 → 𝐵 = 𝐶)) | 
| 23 | 16, 22 | sylbi 217 | . . . . 5
⊢ ({𝐴, 𝐵} = {𝐶, 𝐷} → (𝐴 = 𝐷 → 𝐵 = 𝐶)) | 
| 24 | 23 | ancld 550 | . . . 4
⊢ ({𝐴, 𝐵} = {𝐶, 𝐷} → (𝐴 = 𝐷 → (𝐴 = 𝐷 ∧ 𝐵 = 𝐶))) | 
| 25 | 14, 24 | orim12d 966 | . . 3
⊢ ({𝐴, 𝐵} = {𝐶, 𝐷} → ((𝐴 = 𝐶 ∨ 𝐴 = 𝐷) → ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) ∨ (𝐴 = 𝐷 ∧ 𝐵 = 𝐶)))) | 
| 26 | 6, 25 | mpd 15 | . 2
⊢ ({𝐴, 𝐵} = {𝐶, 𝐷} → ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) ∨ (𝐴 = 𝐷 ∧ 𝐵 = 𝐶))) | 
| 27 |  | preq12 4734 | . . 3
⊢ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) → {𝐴, 𝐵} = {𝐶, 𝐷}) | 
| 28 |  | preq12 4734 | . . . 4
⊢ ((𝐴 = 𝐷 ∧ 𝐵 = 𝐶) → {𝐴, 𝐵} = {𝐷, 𝐶}) | 
| 29 |  | prcom 4731 | . . . 4
⊢ {𝐷, 𝐶} = {𝐶, 𝐷} | 
| 30 | 28, 29 | eqtrdi 2792 | . . 3
⊢ ((𝐴 = 𝐷 ∧ 𝐵 = 𝐶) → {𝐴, 𝐵} = {𝐶, 𝐷}) | 
| 31 | 27, 30 | jaoi 857 | . 2
⊢ (((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) ∨ (𝐴 = 𝐷 ∧ 𝐵 = 𝐶)) → {𝐴, 𝐵} = {𝐶, 𝐷}) | 
| 32 | 26, 31 | impbii 209 | 1
⊢ ({𝐴, 𝐵} = {𝐶, 𝐷} ↔ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) ∨ (𝐴 = 𝐷 ∧ 𝐵 = 𝐶))) |