Theorem prel12g 4865

Description: Equality of two unordered pairs. (Contributed by NM, 17-Oct-1996.) (Revised by AV, 9-Dec-2018.) (Revised by AV, 12-Jun-2022.)

Assertion

Ref	Expression
prel12g	⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) → ({𝐴, 𝐵} = {𝐶, 𝐷} ↔ (𝐴 ∈ {𝐶, 𝐷} ∧ 𝐵 ∈ {𝐶, 𝐷})))

Proof of Theorem prel12g

Step	Hyp	Ref	Expression
1		preq12nebg 4864	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) → ({𝐴, 𝐵} = {𝐶, 𝐷} ↔ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) ∨ (𝐴 = 𝐷 ∧ 𝐵 = 𝐶))))
2		prid1g 4765	. . . . . . . . 9 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ {𝐴, 𝐷})
3	2	3ad2ant1 1134	. . . . . . . 8 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) → 𝐴 ∈ {𝐴, 𝐷})
4	3	adantr 482	. . . . . . 7 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ 𝐴 = 𝐶) → 𝐴 ∈ {𝐴, 𝐷})
5		preq1 4738	. . . . . . . 8 ⊢ (𝐴 = 𝐶 → {𝐴, 𝐷} = {𝐶, 𝐷})
6	5	adantl 483	. . . . . . 7 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ 𝐴 = 𝐶) → {𝐴, 𝐷} = {𝐶, 𝐷})
7	4, 6	eleqtrd 2836	. . . . . 6 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ 𝐴 = 𝐶) → 𝐴 ∈ {𝐶, 𝐷})
8	7	ex 414	. . . . 5 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) → (𝐴 = 𝐶 → 𝐴 ∈ {𝐶, 𝐷}))
9		prid2g 4766	. . . . . . 7 ⊢ (𝐵 ∈ 𝑊 → 𝐵 ∈ {𝐶, 𝐵})
10	9	3ad2ant2 1135	. . . . . 6 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) → 𝐵 ∈ {𝐶, 𝐵})
11		preq2 4739	. . . . . . 7 ⊢ (𝐵 = 𝐷 → {𝐶, 𝐵} = {𝐶, 𝐷})
12	11	eleq2d 2820	. . . . . 6 ⊢ (𝐵 = 𝐷 → (𝐵 ∈ {𝐶, 𝐵} ↔ 𝐵 ∈ {𝐶, 𝐷}))
13	10, 12	syl5ibcom 244	. . . . 5 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) → (𝐵 = 𝐷 → 𝐵 ∈ {𝐶, 𝐷}))
14	8, 13	anim12d 610	. . . 4 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) → ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) → (𝐴 ∈ {𝐶, 𝐷} ∧ 𝐵 ∈ {𝐶, 𝐷})))
15		prid2g 4766	. . . . . . 7 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ {𝐶, 𝐴})
16	15	3ad2ant1 1134	. . . . . 6 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) → 𝐴 ∈ {𝐶, 𝐴})
17		preq2 4739	. . . . . . 7 ⊢ (𝐴 = 𝐷 → {𝐶, 𝐴} = {𝐶, 𝐷})
18	17	eleq2d 2820	. . . . . 6 ⊢ (𝐴 = 𝐷 → (𝐴 ∈ {𝐶, 𝐴} ↔ 𝐴 ∈ {𝐶, 𝐷}))
19	16, 18	syl5ibcom 244	. . . . 5 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) → (𝐴 = 𝐷 → 𝐴 ∈ {𝐶, 𝐷}))
20		prid1g 4765	. . . . . . 7 ⊢ (𝐵 ∈ 𝑊 → 𝐵 ∈ {𝐵, 𝐷})
21	20	3ad2ant2 1135	. . . . . 6 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) → 𝐵 ∈ {𝐵, 𝐷})
22		preq1 4738	. . . . . . 7 ⊢ (𝐵 = 𝐶 → {𝐵, 𝐷} = {𝐶, 𝐷})
23	22	eleq2d 2820	. . . . . 6 ⊢ (𝐵 = 𝐶 → (𝐵 ∈ {𝐵, 𝐷} ↔ 𝐵 ∈ {𝐶, 𝐷}))
24	21, 23	syl5ibcom 244	. . . . 5 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) → (𝐵 = 𝐶 → 𝐵 ∈ {𝐶, 𝐷}))
25	19, 24	anim12d 610	. . . 4 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) → ((𝐴 = 𝐷 ∧ 𝐵 = 𝐶) → (𝐴 ∈ {𝐶, 𝐷} ∧ 𝐵 ∈ {𝐶, 𝐷})))
26	14, 25	jaod 858	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) → (((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) ∨ (𝐴 = 𝐷 ∧ 𝐵 = 𝐶)) → (𝐴 ∈ {𝐶, 𝐷} ∧ 𝐵 ∈ {𝐶, 𝐷})))
27		elprg 4650	. . . . . 6 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ {𝐶, 𝐷} ↔ (𝐴 = 𝐶 ∨ 𝐴 = 𝐷)))
28	27	3ad2ant1 1134	. . . . 5 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) → (𝐴 ∈ {𝐶, 𝐷} ↔ (𝐴 = 𝐶 ∨ 𝐴 = 𝐷)))
29		elprg 4650	. . . . . 6 ⊢ (𝐵 ∈ 𝑊 → (𝐵 ∈ {𝐶, 𝐷} ↔ (𝐵 = 𝐶 ∨ 𝐵 = 𝐷)))
30	29	3ad2ant2 1135	. . . . 5 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) → (𝐵 ∈ {𝐶, 𝐷} ↔ (𝐵 = 𝐶 ∨ 𝐵 = 𝐷)))
31	28, 30	anbi12d 632	. . . 4 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) → ((𝐴 ∈ {𝐶, 𝐷} ∧ 𝐵 ∈ {𝐶, 𝐷}) ↔ ((𝐴 = 𝐶 ∨ 𝐴 = 𝐷) ∧ (𝐵 = 𝐶 ∨ 𝐵 = 𝐷))))
32		eqtr3 2759	. . . . . . . 8 ⊢ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐶) → 𝐴 = 𝐵)
33		eqneqall 2952	. . . . . . . 8 ⊢ (𝐴 = 𝐵 → (𝐴 ≠ 𝐵 → ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) ∨ (𝐴 = 𝐷 ∧ 𝐵 = 𝐶))))
34	32, 33	syl 17	. . . . . . 7 ⊢ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐶) → (𝐴 ≠ 𝐵 → ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) ∨ (𝐴 = 𝐷 ∧ 𝐵 = 𝐶))))
35		olc 867	. . . . . . . 8 ⊢ ((𝐴 = 𝐷 ∧ 𝐵 = 𝐶) → ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) ∨ (𝐴 = 𝐷 ∧ 𝐵 = 𝐶)))
36	35	a1d 25	. . . . . . 7 ⊢ ((𝐴 = 𝐷 ∧ 𝐵 = 𝐶) → (𝐴 ≠ 𝐵 → ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) ∨ (𝐴 = 𝐷 ∧ 𝐵 = 𝐶))))
37		orc 866	. . . . . . . 8 ⊢ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) → ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) ∨ (𝐴 = 𝐷 ∧ 𝐵 = 𝐶)))
38	37	a1d 25	. . . . . . 7 ⊢ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) → (𝐴 ≠ 𝐵 → ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) ∨ (𝐴 = 𝐷 ∧ 𝐵 = 𝐶))))
39		eqtr3 2759	. . . . . . . 8 ⊢ ((𝐴 = 𝐷 ∧ 𝐵 = 𝐷) → 𝐴 = 𝐵)
40	39, 33	syl 17	. . . . . . 7 ⊢ ((𝐴 = 𝐷 ∧ 𝐵 = 𝐷) → (𝐴 ≠ 𝐵 → ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) ∨ (𝐴 = 𝐷 ∧ 𝐵 = 𝐶))))
41	34, 36, 38, 40	ccase 1037	. . . . . 6 ⊢ (((𝐴 = 𝐶 ∨ 𝐴 = 𝐷) ∧ (𝐵 = 𝐶 ∨ 𝐵 = 𝐷)) → (𝐴 ≠ 𝐵 → ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) ∨ (𝐴 = 𝐷 ∧ 𝐵 = 𝐶))))
42	41	com12 32	. . . . 5 ⊢ (𝐴 ≠ 𝐵 → (((𝐴 = 𝐶 ∨ 𝐴 = 𝐷) ∧ (𝐵 = 𝐶 ∨ 𝐵 = 𝐷)) → ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) ∨ (𝐴 = 𝐷 ∧ 𝐵 = 𝐶))))
43	42	3ad2ant3 1136	. . . 4 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) → (((𝐴 = 𝐶 ∨ 𝐴 = 𝐷) ∧ (𝐵 = 𝐶 ∨ 𝐵 = 𝐷)) → ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) ∨ (𝐴 = 𝐷 ∧ 𝐵 = 𝐶))))
44	31, 43	sylbid 239	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) → ((𝐴 ∈ {𝐶, 𝐷} ∧ 𝐵 ∈ {𝐶, 𝐷}) → ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) ∨ (𝐴 = 𝐷 ∧ 𝐵 = 𝐶))))
45	26, 44	impbid 211	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) → (((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) ∨ (𝐴 = 𝐷 ∧ 𝐵 = 𝐶)) ↔ (𝐴 ∈ {𝐶, 𝐷} ∧ 𝐵 ∈ {𝐶, 𝐷})))
46	1, 45	bitrd 279	1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) → ({𝐴, 𝐵} = {𝐶, 𝐷} ↔ (𝐴 ∈ {𝐶, 𝐷} ∧ 𝐵 ∈ {𝐶, 𝐷})))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 397   ∨ wo 846   ∧ w3a 1088   = wceq 1542   ∈ wcel 2107   ≠ wne 2941  {cpr 4631

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ne 2942  df-v 3477  df-dif 3952  df-un 3954  df-nul 4324  df-sn 4630  df-pr 4632

This theorem is referenced by:  dfac2b  10125  hash2prd  14436