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	⊢ ( ( ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑋 ) ∧ 𝐴 ≠ 𝐵 ) → ( 𝐴 = 𝐶 ↔ { 𝐴 , 𝐵 } = { 𝐵 , 𝐶 } ) )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ 𝐵 = 𝐵
2	1	biantru	⊢ ( 𝐴 = 𝐶 ↔ ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐵 ) )
3	2	orbi2i	⊢ ( ( ( 𝐴 = 𝐵 ∧ 𝐵 = 𝐶 ) ∨ 𝐴 = 𝐶 ) ↔ ( ( 𝐴 = 𝐵 ∧ 𝐵 = 𝐶 ) ∨ ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐵 ) ) )
4	3	a1i	⊢ ( ( ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑋 ) ∧ 𝐴 ≠ 𝐵 ) → ( ( ( 𝐴 = 𝐵 ∧ 𝐵 = 𝐶 ) ∨ 𝐴 = 𝐶 ) ↔ ( ( 𝐴 = 𝐵 ∧ 𝐵 = 𝐶 ) ∨ ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐵 ) ) ) )
5		neneq	⊢ ( 𝐴 ≠ 𝐵 → ¬ 𝐴 = 𝐵 )
6	5	adantl	⊢ ( ( ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑋 ) ∧ 𝐴 ≠ 𝐵 ) → ¬ 𝐴 = 𝐵 )
7	6	intnanrd	⊢ ( ( ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑋 ) ∧ 𝐴 ≠ 𝐵 ) → ¬ ( 𝐴 = 𝐵 ∧ 𝐵 = 𝐶 ) )
8		biorf	⊢ ( ¬ ( 𝐴 = 𝐵 ∧ 𝐵 = 𝐶 ) → ( 𝐴 = 𝐶 ↔ ( ( 𝐴 = 𝐵 ∧ 𝐵 = 𝐶 ) ∨ 𝐴 = 𝐶 ) ) )
9	7 8	syl	⊢ ( ( ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑋 ) ∧ 𝐴 ≠ 𝐵 ) → ( 𝐴 = 𝐶 ↔ ( ( 𝐴 = 𝐵 ∧ 𝐵 = 𝐶 ) ∨ 𝐴 = 𝐶 ) ) )
10		3simpa	⊢ ( ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑋 ) → ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ) )
11		3simpc	⊢ ( ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑋 ) → ( 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑋 ) )
12	10 11	jca	⊢ ( ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑋 ) → ( ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑋 ) ) )
13	12	adantr	⊢ ( ( ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑋 ) ∧ 𝐴 ≠ 𝐵 ) → ( ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑋 ) ) )
14		preq12bg	⊢ ( ( ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑋 ) ) → ( { 𝐴 , 𝐵 } = { 𝐵 , 𝐶 } ↔ ( ( 𝐴 = 𝐵 ∧ 𝐵 = 𝐶 ) ∨ ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐵 ) ) ) )
15	13 14	syl	⊢ ( ( ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑋 ) ∧ 𝐴 ≠ 𝐵 ) → ( { 𝐴 , 𝐵 } = { 𝐵 , 𝐶 } ↔ ( ( 𝐴 = 𝐵 ∧ 𝐵 = 𝐶 ) ∨ ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐵 ) ) ) )
16	4 9 15	3bitr4d	⊢ ( ( ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑋 ) ∧ 𝐴 ≠ 𝐵 ) → ( 𝐴 = 𝐶 ↔ { 𝐴 , 𝐵 } = { 𝐵 , 𝐶 } ) )