Metamath Proof Explorer

Theorem pr1eqbg

Description: A (proper) pair is equal to another (maybe improper) pair containing one element of the first pair if and only if the other element of the first pair is contained in the second pair. (Contributed by Alexander van der Vekens, 26-Jan-2018)

Ref Expression
Assertion pr1eqbg ⊢ A ∈ U ∧ B ∈ V ∧ C ∈ X ∧ A ≠ B → A = C ↔ A B = B C

Proof

Step Hyp Ref Expression
1 eqid ⊢ B = B
2 1 biantru ⊢ A = C ↔ A = C ∧ B = B
3 2 orbi2i ⊢ A = B ∧ B = C ∨ A = C ↔ A = B ∧ B = C ∨ A = C ∧ B = B
4 3 a1i ⊢ A ∈ U ∧ B ∈ V ∧ C ∈ X ∧ A ≠ B → A = B ∧ B = C ∨ A = C ↔ A = B ∧ B = C ∨ A = C ∧ B = B
5 neneq ⊢ A ≠ B → ¬ A = B
6 5 adantl ⊢ A ∈ U ∧ B ∈ V ∧ C ∈ X ∧ A ≠ B → ¬ A = B
7 6 intnanrd ⊢ A ∈ U ∧ B ∈ V ∧ C ∈ X ∧ A ≠ B → ¬ A = B ∧ B = C
8 biorf ⊢ ¬ A = B ∧ B = C → A = C ↔ A = B ∧ B = C ∨ A = C
9 7 8 syl ⊢ A ∈ U ∧ B ∈ V ∧ C ∈ X ∧ A ≠ B → A = C ↔ A = B ∧ B = C ∨ A = C
10 3simpa ⊢ A ∈ U ∧ B ∈ V ∧ C ∈ X → A ∈ U ∧ B ∈ V
11 3simpc ⊢ A ∈ U ∧ B ∈ V ∧ C ∈ X → B ∈ V ∧ C ∈ X
12 10 11 jca ⊢ A ∈ U ∧ B ∈ V ∧ C ∈ X → A ∈ U ∧ B ∈ V ∧ B ∈ V ∧ C ∈ X
13 12 adantr ⊢ A ∈ U ∧ B ∈ V ∧ C ∈ X ∧ A ≠ B → A ∈ U ∧ B ∈ V ∧ B ∈ V ∧ C ∈ X
14 preq12bg ⊢ A ∈ U ∧ B ∈ V ∧ B ∈ V ∧ C ∈ X → A B = B C ↔ A = B ∧ B = C ∨ A = C ∧ B = B
15 13 14 syl ⊢ A ∈ U ∧ B ∈ V ∧ C ∈ X ∧ A ≠ B → A B = B C ↔ A = B ∧ B = C ∨ A = C ∧ B = B
16 4 9 15 3bitr4d ⊢ A ∈ U ∧ B ∈ V ∧ C ∈ X ∧ A ≠ B → A = C ↔ A B = B C