Theorem pr1eqbg 4833

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 2735	. . . . 5 ⊢ 𝐵 = 𝐵
2	1	biantru 529	. . . 4 ⊢ (𝐴 = 𝐶 ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐵))
3	2	orbi2i 912	. . 3 ⊢ (((𝐴 = 𝐵 ∧ 𝐵 = 𝐶) ∨ 𝐴 = 𝐶) ↔ ((𝐴 = 𝐵 ∧ 𝐵 = 𝐶) ∨ (𝐴 = 𝐶 ∧ 𝐵 = 𝐵)))
4	3	a1i 11	. 2 ⊢ (((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑋) ∧ 𝐴 ≠ 𝐵) → (((𝐴 = 𝐵 ∧ 𝐵 = 𝐶) ∨ 𝐴 = 𝐶) ↔ ((𝐴 = 𝐵 ∧ 𝐵 = 𝐶) ∨ (𝐴 = 𝐶 ∧ 𝐵 = 𝐵))))
5		neneq 2938	. . . . 5 ⊢ (𝐴 ≠ 𝐵 → ¬ 𝐴 = 𝐵)
6	5	adantl 481	. . . 4 ⊢ (((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑋) ∧ 𝐴 ≠ 𝐵) → ¬ 𝐴 = 𝐵)
7	6	intnanrd 489	. . 3 ⊢ (((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑋) ∧ 𝐴 ≠ 𝐵) → ¬ (𝐴 = 𝐵 ∧ 𝐵 = 𝐶))
8		biorf 936	. . 3 ⊢ (¬ (𝐴 = 𝐵 ∧ 𝐵 = 𝐶) → (𝐴 = 𝐶 ↔ ((𝐴 = 𝐵 ∧ 𝐵 = 𝐶) ∨ 𝐴 = 𝐶)))
9	7, 8	syl 17	. 2 ⊢ (((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑋) ∧ 𝐴 ≠ 𝐵) → (𝐴 = 𝐶 ↔ ((𝐴 = 𝐵 ∧ 𝐵 = 𝐶) ∨ 𝐴 = 𝐶)))
10		3simpa 1148	. . . . 5 ⊢ ((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑋) → (𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉))
11		3simpc 1150	. . . . 5 ⊢ ((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑋) → (𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑋))
12	10, 11	jca 511	. . . 4 ⊢ ((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑋) → ((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉) ∧ (𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑋)))
13	12	adantr 480	. . 3 ⊢ (((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑋) ∧ 𝐴 ≠ 𝐵) → ((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉) ∧ (𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑋)))
14		preq12bg 4829	. . 3 ⊢ (((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉) ∧ (𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑋)) → ({𝐴, 𝐵} = {𝐵, 𝐶} ↔ ((𝐴 = 𝐵 ∧ 𝐵 = 𝐶) ∨ (𝐴 = 𝐶 ∧ 𝐵 = 𝐵))))
15	13, 14	syl 17	. 2 ⊢ (((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑋) ∧ 𝐴 ≠ 𝐵) → ({𝐴, 𝐵} = {𝐵, 𝐶} ↔ ((𝐴 = 𝐵 ∧ 𝐵 = 𝐶) ∨ (𝐴 = 𝐶 ∧ 𝐵 = 𝐵))))
16	4, 9, 15	3bitr4d 311	1 ⊢ (((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑋) ∧ 𝐴 ≠ 𝐵) → (𝐴 = 𝐶 ↔ {𝐴, 𝐵} = {𝐵, 𝐶}))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 847   ∧ w3a 1086   = wceq 1540   ∈ wcel 2108   ≠ wne 2932  {cpr 4603

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-ne 2933  df-v 3461  df-un 3931  df-sn 4602  df-pr 4604

This theorem is referenced by:  pr1nebg  4834