Proof of Theorem pr1eqbg
| Step | Hyp | Ref
| Expression |
| 1 | | eqid 2737 |
. . . . 5
⊢ 𝐵 = 𝐵 |
| 2 | 1 | biantru 529 |
. . . 4
⊢ (𝐴 = 𝐶 ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐵)) |
| 3 | 2 | orbi2i 913 |
. . 3
⊢ (((𝐴 = 𝐵 ∧ 𝐵 = 𝐶) ∨ 𝐴 = 𝐶) ↔ ((𝐴 = 𝐵 ∧ 𝐵 = 𝐶) ∨ (𝐴 = 𝐶 ∧ 𝐵 = 𝐵))) |
| 4 | 3 | a1i 11 |
. 2
⊢ (((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑋) ∧ 𝐴 ≠ 𝐵) → (((𝐴 = 𝐵 ∧ 𝐵 = 𝐶) ∨ 𝐴 = 𝐶) ↔ ((𝐴 = 𝐵 ∧ 𝐵 = 𝐶) ∨ (𝐴 = 𝐶 ∧ 𝐵 = 𝐵)))) |
| 5 | | neneq 2946 |
. . . . 5
⊢ (𝐴 ≠ 𝐵 → ¬ 𝐴 = 𝐵) |
| 6 | 5 | adantl 481 |
. . . 4
⊢ (((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑋) ∧ 𝐴 ≠ 𝐵) → ¬ 𝐴 = 𝐵) |
| 7 | 6 | intnanrd 489 |
. . 3
⊢ (((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑋) ∧ 𝐴 ≠ 𝐵) → ¬ (𝐴 = 𝐵 ∧ 𝐵 = 𝐶)) |
| 8 | | biorf 937 |
. . 3
⊢ (¬
(𝐴 = 𝐵 ∧ 𝐵 = 𝐶) → (𝐴 = 𝐶 ↔ ((𝐴 = 𝐵 ∧ 𝐵 = 𝐶) ∨ 𝐴 = 𝐶))) |
| 9 | 7, 8 | syl 17 |
. 2
⊢ (((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑋) ∧ 𝐴 ≠ 𝐵) → (𝐴 = 𝐶 ↔ ((𝐴 = 𝐵 ∧ 𝐵 = 𝐶) ∨ 𝐴 = 𝐶))) |
| 10 | | 3simpa 1149 |
. . . . 5
⊢ ((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑋) → (𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉)) |
| 11 | | 3simpc 1151 |
. . . . 5
⊢ ((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑋) → (𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑋)) |
| 12 | 10, 11 | jca 511 |
. . . 4
⊢ ((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑋) → ((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉) ∧ (𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑋))) |
| 13 | 12 | adantr 480 |
. . 3
⊢ (((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑋) ∧ 𝐴 ≠ 𝐵) → ((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉) ∧ (𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑋))) |
| 14 | | preq12bg 4853 |
. . 3
⊢ (((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉) ∧ (𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑋)) → ({𝐴, 𝐵} = {𝐵, 𝐶} ↔ ((𝐴 = 𝐵 ∧ 𝐵 = 𝐶) ∨ (𝐴 = 𝐶 ∧ 𝐵 = 𝐵)))) |
| 15 | 13, 14 | syl 17 |
. 2
⊢ (((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑋) ∧ 𝐴 ≠ 𝐵) → ({𝐴, 𝐵} = {𝐵, 𝐶} ↔ ((𝐴 = 𝐵 ∧ 𝐵 = 𝐶) ∨ (𝐴 = 𝐶 ∧ 𝐵 = 𝐵)))) |
| 16 | 4, 9, 15 | 3bitr4d 311 |
1
⊢ (((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑋) ∧ 𝐴 ≠ 𝐵) → (𝐴 = 𝐶 ↔ {𝐴, 𝐵} = {𝐵, 𝐶})) |