Theorem pr1eqbg 4856

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 2730	. . . . 5 ⊢ 𝐵 = 𝐵
2	1	biantru 528	. . . 4 ⊢ (𝐴 = 𝐶 ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐵))
3	2	orbi2i 909	. . 3 ⊢ (((𝐴 = 𝐵 ∧ 𝐵 = 𝐶) ∨ 𝐴 = 𝐶) ↔ ((𝐴 = 𝐵 ∧ 𝐵 = 𝐶) ∨ (𝐴 = 𝐶 ∧ 𝐵 = 𝐵)))
4	3	a1i 11	. 2 ⊢ (((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑋) ∧ 𝐴 ≠ 𝐵) → (((𝐴 = 𝐵 ∧ 𝐵 = 𝐶) ∨ 𝐴 = 𝐶) ↔ ((𝐴 = 𝐵 ∧ 𝐵 = 𝐶) ∨ (𝐴 = 𝐶 ∧ 𝐵 = 𝐵))))
5		neneq 2944	. . . . 5 ⊢ (𝐴 ≠ 𝐵 → ¬ 𝐴 = 𝐵)
6	5	adantl 480	. . . 4 ⊢ (((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑋) ∧ 𝐴 ≠ 𝐵) → ¬ 𝐴 = 𝐵)
7	6	intnanrd 488	. . 3 ⊢ (((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑋) ∧ 𝐴 ≠ 𝐵) → ¬ (𝐴 = 𝐵 ∧ 𝐵 = 𝐶))
8		biorf 933	. . 3 ⊢ (¬ (𝐴 = 𝐵 ∧ 𝐵 = 𝐶) → (𝐴 = 𝐶 ↔ ((𝐴 = 𝐵 ∧ 𝐵 = 𝐶) ∨ 𝐴 = 𝐶)))
9	7, 8	syl 17	. 2 ⊢ (((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑋) ∧ 𝐴 ≠ 𝐵) → (𝐴 = 𝐶 ↔ ((𝐴 = 𝐵 ∧ 𝐵 = 𝐶) ∨ 𝐴 = 𝐶)))
10		3simpa 1146	. . . . 5 ⊢ ((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑋) → (𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉))
11		3simpc 1148	. . . . 5 ⊢ ((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑋) → (𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑋))
12	10, 11	jca 510	. . . 4 ⊢ ((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑋) → ((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉) ∧ (𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑋)))
13	12	adantr 479	. . 3 ⊢ (((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑋) ∧ 𝐴 ≠ 𝐵) → ((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉) ∧ (𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑋)))
14		preq12bg 4853	. . 3 ⊢ (((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉) ∧ (𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑋)) → ({𝐴, 𝐵} = {𝐵, 𝐶} ↔ ((𝐴 = 𝐵 ∧ 𝐵 = 𝐶) ∨ (𝐴 = 𝐶 ∧ 𝐵 = 𝐵))))
15	13, 14	syl 17	. 2 ⊢ (((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑋) ∧ 𝐴 ≠ 𝐵) → ({𝐴, 𝐵} = {𝐵, 𝐶} ↔ ((𝐴 = 𝐵 ∧ 𝐵 = 𝐶) ∨ (𝐴 = 𝐶 ∧ 𝐵 = 𝐵))))
16	4, 9, 15	3bitr4d 310	1 ⊢ (((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑋) ∧ 𝐴 ≠ 𝐵) → (𝐴 = 𝐶 ↔ {𝐴, 𝐵} = {𝐵, 𝐶}))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 394   ∨ wo 843   ∧ w3a 1085   = wceq 1539   ∈ wcel 2104   ≠ wne 2938  {cpr 4629

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3an 1087  df-tru 1542  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-ne 2939  df-v 3474  df-un 3952  df-sn 4628  df-pr 4630

This theorem is referenced by:  pr1nebg  4857