Theorem pr1eqbg 4784

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.)

Assertion

Ref	Expression
pr1eqbg	⊢ (((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑋) ∧ 𝐴 ≠ 𝐵) → (𝐴 = 𝐶 ↔ {𝐴, 𝐵} = {𝐵, 𝐶}))

Proof of Theorem pr1eqbg

Step	Hyp	Ref	Expression
1		eqid 2738	. . . . 5 ⊢ 𝐵 = 𝐵
2	1	biantru 529	. . . 4 ⊢ (𝐴 = 𝐶 ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐵))
3	2	orbi2i 909	. . 3 ⊢ (((𝐴 = 𝐵 ∧ 𝐵 = 𝐶) ∨ 𝐴 = 𝐶) ↔ ((𝐴 = 𝐵 ∧ 𝐵 = 𝐶) ∨ (𝐴 = 𝐶 ∧ 𝐵 = 𝐵)))
4	3	a1i 11	. 2 ⊢ (((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑋) ∧ 𝐴 ≠ 𝐵) → (((𝐴 = 𝐵 ∧ 𝐵 = 𝐶) ∨ 𝐴 = 𝐶) ↔ ((𝐴 = 𝐵 ∧ 𝐵 = 𝐶) ∨ (𝐴 = 𝐶 ∧ 𝐵 = 𝐵))))
5		neneq 2948	. . . . 5 ⊢ (𝐴 ≠ 𝐵 → ¬ 𝐴 = 𝐵)
6	5	adantl 481	. . . 4 ⊢ (((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑋) ∧ 𝐴 ≠ 𝐵) → ¬ 𝐴 = 𝐵)
7	6	intnanrd 489	. . 3 ⊢ (((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑋) ∧ 𝐴 ≠ 𝐵) → ¬ (𝐴 = 𝐵 ∧ 𝐵 = 𝐶))
8		biorf 933	. . 3 ⊢ (¬ (𝐴 = 𝐵 ∧ 𝐵 = 𝐶) → (𝐴 = 𝐶 ↔ ((𝐴 = 𝐵 ∧ 𝐵 = 𝐶) ∨ 𝐴 = 𝐶)))
9	7, 8	syl 17	. 2 ⊢ (((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑋) ∧ 𝐴 ≠ 𝐵) → (𝐴 = 𝐶 ↔ ((𝐴 = 𝐵 ∧ 𝐵 = 𝐶) ∨ 𝐴 = 𝐶)))
10		3simpa 1146	. . . . 5 ⊢ ((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑋) → (𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉))
11		3simpc 1148	. . . . 5 ⊢ ((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑋) → (𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑋))
12	10, 11	jca 511	. . . 4 ⊢ ((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑋) → ((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉) ∧ (𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑋)))
13	12	adantr 480	. . 3 ⊢ (((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑋) ∧ 𝐴 ≠ 𝐵) → ((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉) ∧ (𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑋)))
14		preq12bg 4781	. . 3 ⊢ (((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉) ∧ (𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑋)) → ({𝐴, 𝐵} = {𝐵, 𝐶} ↔ ((𝐴 = 𝐵 ∧ 𝐵 = 𝐶) ∨ (𝐴 = 𝐶 ∧ 𝐵 = 𝐵))))
15	13, 14	syl 17	. 2 ⊢ (((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑋) ∧ 𝐴 ≠ 𝐵) → ({𝐴, 𝐵} = {𝐵, 𝐶} ↔ ((𝐴 = 𝐵 ∧ 𝐵 = 𝐶) ∨ (𝐴 = 𝐶 ∧ 𝐵 = 𝐵))))
16	4, 9, 15	3bitr4d 310	1 ⊢ (((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑋) ∧ 𝐴 ≠ 𝐵) → (𝐴 = 𝐶 ↔ {𝐴, 𝐵} = {𝐵, 𝐶}))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 395   ∨ wo 843   ∧ w3a 1085   = wceq 1539   ∈ wcel 2108   ≠ wne 2942  {cpr 4560

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-ne 2943  df-v 3424  df-un 3888  df-sn 4559  df-pr 4561

This theorem is referenced by:  pr1nebg  4785