Theorem pr1eqbg 4821

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 2729	. . . . 5 ⊢ 𝐵 = 𝐵
2	1	biantru 529	. . . 4 ⊢ (𝐴 = 𝐶 ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐵))
3	2	orbi2i 912	. . 3 ⊢ (((𝐴 = 𝐵 ∧ 𝐵 = 𝐶) ∨ 𝐴 = 𝐶) ↔ ((𝐴 = 𝐵 ∧ 𝐵 = 𝐶) ∨ (𝐴 = 𝐶 ∧ 𝐵 = 𝐵)))
4	3	a1i 11	. 2 ⊢ (((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑋) ∧ 𝐴 ≠ 𝐵) → (((𝐴 = 𝐵 ∧ 𝐵 = 𝐶) ∨ 𝐴 = 𝐶) ↔ ((𝐴 = 𝐵 ∧ 𝐵 = 𝐶) ∨ (𝐴 = 𝐶 ∧ 𝐵 = 𝐵))))
5		neneq 2931	. . . . 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 4817	. . 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 2109   ≠ wne 2925  {cpr 4591

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701

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 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-v 3449  df-un 3919  df-sn 4590  df-pr 4592

This theorem is referenced by:  pr1nebg  4822