Theorem preq12bg 4829

Description: Closed form of preq12b 4826. (Contributed by Scott Fenton, 28-Mar-2014.)

Assertion

Ref	Expression
preq12bg	⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ (𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌)) → ({𝐴, 𝐵} = {𝐶, 𝐷} ↔ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) ∨ (𝐴 = 𝐷 ∧ 𝐵 = 𝐶))))

Proof of Theorem preq12bg

Dummy variables 𝑥 𝑦 𝑧 𝑤 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		preq1 4709	. . . . . . 7 ⊢ (𝑥 = 𝐴 → {𝑥, 𝑦} = {𝐴, 𝑦})
2	1	eqeq1d 2737	. . . . . 6 ⊢ (𝑥 = 𝐴 → ({𝑥, 𝑦} = {𝑧, 𝐷} ↔ {𝐴, 𝑦} = {𝑧, 𝐷}))
3		eqeq1 2739	. . . . . . . 8 ⊢ (𝑥 = 𝐴 → (𝑥 = 𝑧 ↔ 𝐴 = 𝑧))
4	3	anbi1d 631	. . . . . . 7 ⊢ (𝑥 = 𝐴 → ((𝑥 = 𝑧 ∧ 𝑦 = 𝐷) ↔ (𝐴 = 𝑧 ∧ 𝑦 = 𝐷)))
5		eqeq1 2739	. . . . . . . 8 ⊢ (𝑥 = 𝐴 → (𝑥 = 𝐷 ↔ 𝐴 = 𝐷))
6	5	anbi1d 631	. . . . . . 7 ⊢ (𝑥 = 𝐴 → ((𝑥 = 𝐷 ∧ 𝑦 = 𝑧) ↔ (𝐴 = 𝐷 ∧ 𝑦 = 𝑧)))
7	4, 6	orbi12d 918	. . . . . 6 ⊢ (𝑥 = 𝐴 → (((𝑥 = 𝑧 ∧ 𝑦 = 𝐷) ∨ (𝑥 = 𝐷 ∧ 𝑦 = 𝑧)) ↔ ((𝐴 = 𝑧 ∧ 𝑦 = 𝐷) ∨ (𝐴 = 𝐷 ∧ 𝑦 = 𝑧))))
8	2, 7	bibi12d 345	. . . . 5 ⊢ (𝑥 = 𝐴 → (({𝑥, 𝑦} = {𝑧, 𝐷} ↔ ((𝑥 = 𝑧 ∧ 𝑦 = 𝐷) ∨ (𝑥 = 𝐷 ∧ 𝑦 = 𝑧))) ↔ ({𝐴, 𝑦} = {𝑧, 𝐷} ↔ ((𝐴 = 𝑧 ∧ 𝑦 = 𝐷) ∨ (𝐴 = 𝐷 ∧ 𝑦 = 𝑧)))))
9	8	imbi2d 340	. . . 4 ⊢ (𝑥 = 𝐴 → ((𝐷 ∈ 𝑌 → ({𝑥, 𝑦} = {𝑧, 𝐷} ↔ ((𝑥 = 𝑧 ∧ 𝑦 = 𝐷) ∨ (𝑥 = 𝐷 ∧ 𝑦 = 𝑧)))) ↔ (𝐷 ∈ 𝑌 → ({𝐴, 𝑦} = {𝑧, 𝐷} ↔ ((𝐴 = 𝑧 ∧ 𝑦 = 𝐷) ∨ (𝐴 = 𝐷 ∧ 𝑦 = 𝑧))))))
10		preq2 4710	. . . . . . 7 ⊢ (𝑦 = 𝐵 → {𝐴, 𝑦} = {𝐴, 𝐵})
11	10	eqeq1d 2737	. . . . . 6 ⊢ (𝑦 = 𝐵 → ({𝐴, 𝑦} = {𝑧, 𝐷} ↔ {𝐴, 𝐵} = {𝑧, 𝐷}))
12		eqeq1 2739	. . . . . . . 8 ⊢ (𝑦 = 𝐵 → (𝑦 = 𝐷 ↔ 𝐵 = 𝐷))
13	12	anbi2d 630	. . . . . . 7 ⊢ (𝑦 = 𝐵 → ((𝐴 = 𝑧 ∧ 𝑦 = 𝐷) ↔ (𝐴 = 𝑧 ∧ 𝐵 = 𝐷)))
14		eqeq1 2739	. . . . . . . 8 ⊢ (𝑦 = 𝐵 → (𝑦 = 𝑧 ↔ 𝐵 = 𝑧))
15	14	anbi2d 630	. . . . . . 7 ⊢ (𝑦 = 𝐵 → ((𝐴 = 𝐷 ∧ 𝑦 = 𝑧) ↔ (𝐴 = 𝐷 ∧ 𝐵 = 𝑧)))
16	13, 15	orbi12d 918	. . . . . 6 ⊢ (𝑦 = 𝐵 → (((𝐴 = 𝑧 ∧ 𝑦 = 𝐷) ∨ (𝐴 = 𝐷 ∧ 𝑦 = 𝑧)) ↔ ((𝐴 = 𝑧 ∧ 𝐵 = 𝐷) ∨ (𝐴 = 𝐷 ∧ 𝐵 = 𝑧))))
17	11, 16	bibi12d 345	. . . . 5 ⊢ (𝑦 = 𝐵 → (({𝐴, 𝑦} = {𝑧, 𝐷} ↔ ((𝐴 = 𝑧 ∧ 𝑦 = 𝐷) ∨ (𝐴 = 𝐷 ∧ 𝑦 = 𝑧))) ↔ ({𝐴, 𝐵} = {𝑧, 𝐷} ↔ ((𝐴 = 𝑧 ∧ 𝐵 = 𝐷) ∨ (𝐴 = 𝐷 ∧ 𝐵 = 𝑧)))))
18	17	imbi2d 340	. . . 4 ⊢ (𝑦 = 𝐵 → ((𝐷 ∈ 𝑌 → ({𝐴, 𝑦} = {𝑧, 𝐷} ↔ ((𝐴 = 𝑧 ∧ 𝑦 = 𝐷) ∨ (𝐴 = 𝐷 ∧ 𝑦 = 𝑧)))) ↔ (𝐷 ∈ 𝑌 → ({𝐴, 𝐵} = {𝑧, 𝐷} ↔ ((𝐴 = 𝑧 ∧ 𝐵 = 𝐷) ∨ (𝐴 = 𝐷 ∧ 𝐵 = 𝑧))))))
19		preq1 4709	. . . . . . 7 ⊢ (𝑧 = 𝐶 → {𝑧, 𝐷} = {𝐶, 𝐷})
20	19	eqeq2d 2746	. . . . . 6 ⊢ (𝑧 = 𝐶 → ({𝐴, 𝐵} = {𝑧, 𝐷} ↔ {𝐴, 𝐵} = {𝐶, 𝐷}))
21		eqeq2 2747	. . . . . . . 8 ⊢ (𝑧 = 𝐶 → (𝐴 = 𝑧 ↔ 𝐴 = 𝐶))
22	21	anbi1d 631	. . . . . . 7 ⊢ (𝑧 = 𝐶 → ((𝐴 = 𝑧 ∧ 𝐵 = 𝐷) ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷)))
23		eqeq2 2747	. . . . . . . 8 ⊢ (𝑧 = 𝐶 → (𝐵 = 𝑧 ↔ 𝐵 = 𝐶))
24	23	anbi2d 630	. . . . . . 7 ⊢ (𝑧 = 𝐶 → ((𝐴 = 𝐷 ∧ 𝐵 = 𝑧) ↔ (𝐴 = 𝐷 ∧ 𝐵 = 𝐶)))
25	22, 24	orbi12d 918	. . . . . 6 ⊢ (𝑧 = 𝐶 → (((𝐴 = 𝑧 ∧ 𝐵 = 𝐷) ∨ (𝐴 = 𝐷 ∧ 𝐵 = 𝑧)) ↔ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) ∨ (𝐴 = 𝐷 ∧ 𝐵 = 𝐶))))
26	20, 25	bibi12d 345	. . . . 5 ⊢ (𝑧 = 𝐶 → (({𝐴, 𝐵} = {𝑧, 𝐷} ↔ ((𝐴 = 𝑧 ∧ 𝐵 = 𝐷) ∨ (𝐴 = 𝐷 ∧ 𝐵 = 𝑧))) ↔ ({𝐴, 𝐵} = {𝐶, 𝐷} ↔ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) ∨ (𝐴 = 𝐷 ∧ 𝐵 = 𝐶)))))
27	26	imbi2d 340	. . . 4 ⊢ (𝑧 = 𝐶 → ((𝐷 ∈ 𝑌 → ({𝐴, 𝐵} = {𝑧, 𝐷} ↔ ((𝐴 = 𝑧 ∧ 𝐵 = 𝐷) ∨ (𝐴 = 𝐷 ∧ 𝐵 = 𝑧)))) ↔ (𝐷 ∈ 𝑌 → ({𝐴, 𝐵} = {𝐶, 𝐷} ↔ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) ∨ (𝐴 = 𝐷 ∧ 𝐵 = 𝐶))))))
28		preq2 4710	. . . . . . 7 ⊢ (𝑤 = 𝐷 → {𝑧, 𝑤} = {𝑧, 𝐷})
29	28	eqeq2d 2746	. . . . . 6 ⊢ (𝑤 = 𝐷 → ({𝑥, 𝑦} = {𝑧, 𝑤} ↔ {𝑥, 𝑦} = {𝑧, 𝐷}))
30		eqeq2 2747	. . . . . . . 8 ⊢ (𝑤 = 𝐷 → (𝑦 = 𝑤 ↔ 𝑦 = 𝐷))
31	30	anbi2d 630	. . . . . . 7 ⊢ (𝑤 = 𝐷 → ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) ↔ (𝑥 = 𝑧 ∧ 𝑦 = 𝐷)))
32		eqeq2 2747	. . . . . . . 8 ⊢ (𝑤 = 𝐷 → (𝑥 = 𝑤 ↔ 𝑥 = 𝐷))
33	32	anbi1d 631	. . . . . . 7 ⊢ (𝑤 = 𝐷 → ((𝑥 = 𝑤 ∧ 𝑦 = 𝑧) ↔ (𝑥 = 𝐷 ∧ 𝑦 = 𝑧)))
34	31, 33	orbi12d 918	. . . . . 6 ⊢ (𝑤 = 𝐷 → (((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) ∨ (𝑥 = 𝑤 ∧ 𝑦 = 𝑧)) ↔ ((𝑥 = 𝑧 ∧ 𝑦 = 𝐷) ∨ (𝑥 = 𝐷 ∧ 𝑦 = 𝑧))))
35		vex 3463	. . . . . . 7 ⊢ 𝑥 ∈ V
36		vex 3463	. . . . . . 7 ⊢ 𝑦 ∈ V
37		vex 3463	. . . . . . 7 ⊢ 𝑧 ∈ V
38		vex 3463	. . . . . . 7 ⊢ 𝑤 ∈ V
39	35, 36, 37, 38	preq12b 4826	. . . . . 6 ⊢ ({𝑥, 𝑦} = {𝑧, 𝑤} ↔ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) ∨ (𝑥 = 𝑤 ∧ 𝑦 = 𝑧)))
40	29, 34, 39	vtoclbg 3536	. . . . 5 ⊢ (𝐷 ∈ 𝑌 → ({𝑥, 𝑦} = {𝑧, 𝐷} ↔ ((𝑥 = 𝑧 ∧ 𝑦 = 𝐷) ∨ (𝑥 = 𝐷 ∧ 𝑦 = 𝑧))))
41	40	a1i 11	. . . 4 ⊢ ((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑊 ∧ 𝑧 ∈ 𝑋) → (𝐷 ∈ 𝑌 → ({𝑥, 𝑦} = {𝑧, 𝐷} ↔ ((𝑥 = 𝑧 ∧ 𝑦 = 𝐷) ∨ (𝑥 = 𝐷 ∧ 𝑦 = 𝑧)))))
42	9, 18, 27, 41	vtocl3ga 3562	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (𝐷 ∈ 𝑌 → ({𝐴, 𝐵} = {𝐶, 𝐷} ↔ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) ∨ (𝐴 = 𝐷 ∧ 𝐵 = 𝐶)))))
43	42	3expa 1118	. 2 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ 𝐶 ∈ 𝑋) → (𝐷 ∈ 𝑌 → ({𝐴, 𝐵} = {𝐶, 𝐷} ↔ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) ∨ (𝐴 = 𝐷 ∧ 𝐵 = 𝐶)))))
44	43	impr 454	1 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ (𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌)) → ({𝐴, 𝐵} = {𝐶, 𝐷} ↔ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) ∨ (𝐴 = 𝐷 ∧ 𝐵 = 𝐶))))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 847   ∧ w3a 1086   = wceq 1540   ∈ wcel 2108  {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-v 3461  df-un 3931  df-sn 4602  df-pr 4604

This theorem is referenced by:  prneimg  4830  prneimg2  4831  pr1eqbg  4833  preqsnd  4835  preq12nebg  4839  opthprneg  4841  preleqALT  9631  pythagtriplem2  16837  pythagtrip  16854  upgrpredgv  29118  uhgr2edg  29187  usgredg2v  29206  2pthon3v  29925  opprb  47060  or2expropbi  47063  ich2exprop  47485  prsprel  47501  paireqne  47525  poprelb  47538  gpgvtxedg0  48067  gpgvtxedg1  48068