Theorem preq12bg 4784

Description: Closed form of preq12b 4781. (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 4669	. . . . . . 7 ⊢ (𝑥 = 𝐴 → {𝑥, 𝑦} = {𝐴, 𝑦})
2	1	eqeq1d 2823	. . . . . 6 ⊢ (𝑥 = 𝐴 → ({𝑥, 𝑦} = {𝑧, 𝐷} ↔ {𝐴, 𝑦} = {𝑧, 𝐷}))
3		eqeq1 2825	. . . . . . . 8 ⊢ (𝑥 = 𝐴 → (𝑥 = 𝑧 ↔ 𝐴 = 𝑧))
4	3	anbi1d 631	. . . . . . 7 ⊢ (𝑥 = 𝐴 → ((𝑥 = 𝑧 ∧ 𝑦 = 𝐷) ↔ (𝐴 = 𝑧 ∧ 𝑦 = 𝐷)))
5		eqeq1 2825	. . . . . . . 8 ⊢ (𝑥 = 𝐴 → (𝑥 = 𝐷 ↔ 𝐴 = 𝐷))
6	5	anbi1d 631	. . . . . . 7 ⊢ (𝑥 = 𝐴 → ((𝑥 = 𝐷 ∧ 𝑦 = 𝑧) ↔ (𝐴 = 𝐷 ∧ 𝑦 = 𝑧)))
7	4, 6	orbi12d 915	. . . . . 6 ⊢ (𝑥 = 𝐴 → (((𝑥 = 𝑧 ∧ 𝑦 = 𝐷) ∨ (𝑥 = 𝐷 ∧ 𝑦 = 𝑧)) ↔ ((𝐴 = 𝑧 ∧ 𝑦 = 𝐷) ∨ (𝐴 = 𝐷 ∧ 𝑦 = 𝑧))))
8	2, 7	bibi12d 348	. . . . 5 ⊢ (𝑥 = 𝐴 → (({𝑥, 𝑦} = {𝑧, 𝐷} ↔ ((𝑥 = 𝑧 ∧ 𝑦 = 𝐷) ∨ (𝑥 = 𝐷 ∧ 𝑦 = 𝑧))) ↔ ({𝐴, 𝑦} = {𝑧, 𝐷} ↔ ((𝐴 = 𝑧 ∧ 𝑦 = 𝐷) ∨ (𝐴 = 𝐷 ∧ 𝑦 = 𝑧)))))
9	8	imbi2d 343	. . . 4 ⊢ (𝑥 = 𝐴 → ((𝐷 ∈ 𝑌 → ({𝑥, 𝑦} = {𝑧, 𝐷} ↔ ((𝑥 = 𝑧 ∧ 𝑦 = 𝐷) ∨ (𝑥 = 𝐷 ∧ 𝑦 = 𝑧)))) ↔ (𝐷 ∈ 𝑌 → ({𝐴, 𝑦} = {𝑧, 𝐷} ↔ ((𝐴 = 𝑧 ∧ 𝑦 = 𝐷) ∨ (𝐴 = 𝐷 ∧ 𝑦 = 𝑧))))))
10		preq2 4670	. . . . . . 7 ⊢ (𝑦 = 𝐵 → {𝐴, 𝑦} = {𝐴, 𝐵})
11	10	eqeq1d 2823	. . . . . 6 ⊢ (𝑦 = 𝐵 → ({𝐴, 𝑦} = {𝑧, 𝐷} ↔ {𝐴, 𝐵} = {𝑧, 𝐷}))
12		eqeq1 2825	. . . . . . . 8 ⊢ (𝑦 = 𝐵 → (𝑦 = 𝐷 ↔ 𝐵 = 𝐷))
13	12	anbi2d 630	. . . . . . 7 ⊢ (𝑦 = 𝐵 → ((𝐴 = 𝑧 ∧ 𝑦 = 𝐷) ↔ (𝐴 = 𝑧 ∧ 𝐵 = 𝐷)))
14		eqeq1 2825	. . . . . . . 8 ⊢ (𝑦 = 𝐵 → (𝑦 = 𝑧 ↔ 𝐵 = 𝑧))
15	14	anbi2d 630	. . . . . . 7 ⊢ (𝑦 = 𝐵 → ((𝐴 = 𝐷 ∧ 𝑦 = 𝑧) ↔ (𝐴 = 𝐷 ∧ 𝐵 = 𝑧)))
16	13, 15	orbi12d 915	. . . . . 6 ⊢ (𝑦 = 𝐵 → (((𝐴 = 𝑧 ∧ 𝑦 = 𝐷) ∨ (𝐴 = 𝐷 ∧ 𝑦 = 𝑧)) ↔ ((𝐴 = 𝑧 ∧ 𝐵 = 𝐷) ∨ (𝐴 = 𝐷 ∧ 𝐵 = 𝑧))))
17	11, 16	bibi12d 348	. . . . 5 ⊢ (𝑦 = 𝐵 → (({𝐴, 𝑦} = {𝑧, 𝐷} ↔ ((𝐴 = 𝑧 ∧ 𝑦 = 𝐷) ∨ (𝐴 = 𝐷 ∧ 𝑦 = 𝑧))) ↔ ({𝐴, 𝐵} = {𝑧, 𝐷} ↔ ((𝐴 = 𝑧 ∧ 𝐵 = 𝐷) ∨ (𝐴 = 𝐷 ∧ 𝐵 = 𝑧)))))
18	17	imbi2d 343	. . . 4 ⊢ (𝑦 = 𝐵 → ((𝐷 ∈ 𝑌 → ({𝐴, 𝑦} = {𝑧, 𝐷} ↔ ((𝐴 = 𝑧 ∧ 𝑦 = 𝐷) ∨ (𝐴 = 𝐷 ∧ 𝑦 = 𝑧)))) ↔ (𝐷 ∈ 𝑌 → ({𝐴, 𝐵} = {𝑧, 𝐷} ↔ ((𝐴 = 𝑧 ∧ 𝐵 = 𝐷) ∨ (𝐴 = 𝐷 ∧ 𝐵 = 𝑧))))))
19		preq1 4669	. . . . . . 7 ⊢ (𝑧 = 𝐶 → {𝑧, 𝐷} = {𝐶, 𝐷})
20	19	eqeq2d 2832	. . . . . 6 ⊢ (𝑧 = 𝐶 → ({𝐴, 𝐵} = {𝑧, 𝐷} ↔ {𝐴, 𝐵} = {𝐶, 𝐷}))
21		eqeq2 2833	. . . . . . . 8 ⊢ (𝑧 = 𝐶 → (𝐴 = 𝑧 ↔ 𝐴 = 𝐶))
22	21	anbi1d 631	. . . . . . 7 ⊢ (𝑧 = 𝐶 → ((𝐴 = 𝑧 ∧ 𝐵 = 𝐷) ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷)))
23		eqeq2 2833	. . . . . . . 8 ⊢ (𝑧 = 𝐶 → (𝐵 = 𝑧 ↔ 𝐵 = 𝐶))
24	23	anbi2d 630	. . . . . . 7 ⊢ (𝑧 = 𝐶 → ((𝐴 = 𝐷 ∧ 𝐵 = 𝑧) ↔ (𝐴 = 𝐷 ∧ 𝐵 = 𝐶)))
25	22, 24	orbi12d 915	. . . . . 6 ⊢ (𝑧 = 𝐶 → (((𝐴 = 𝑧 ∧ 𝐵 = 𝐷) ∨ (𝐴 = 𝐷 ∧ 𝐵 = 𝑧)) ↔ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) ∨ (𝐴 = 𝐷 ∧ 𝐵 = 𝐶))))
26	20, 25	bibi12d 348	. . . . 5 ⊢ (𝑧 = 𝐶 → (({𝐴, 𝐵} = {𝑧, 𝐷} ↔ ((𝐴 = 𝑧 ∧ 𝐵 = 𝐷) ∨ (𝐴 = 𝐷 ∧ 𝐵 = 𝑧))) ↔ ({𝐴, 𝐵} = {𝐶, 𝐷} ↔ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) ∨ (𝐴 = 𝐷 ∧ 𝐵 = 𝐶)))))
27	26	imbi2d 343	. . . 4 ⊢ (𝑧 = 𝐶 → ((𝐷 ∈ 𝑌 → ({𝐴, 𝐵} = {𝑧, 𝐷} ↔ ((𝐴 = 𝑧 ∧ 𝐵 = 𝐷) ∨ (𝐴 = 𝐷 ∧ 𝐵 = 𝑧)))) ↔ (𝐷 ∈ 𝑌 → ({𝐴, 𝐵} = {𝐶, 𝐷} ↔ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) ∨ (𝐴 = 𝐷 ∧ 𝐵 = 𝐶))))))
28		preq2 4670	. . . . . . 7 ⊢ (𝑤 = 𝐷 → {𝑧, 𝑤} = {𝑧, 𝐷})
29	28	eqeq2d 2832	. . . . . 6 ⊢ (𝑤 = 𝐷 → ({𝑥, 𝑦} = {𝑧, 𝑤} ↔ {𝑥, 𝑦} = {𝑧, 𝐷}))
30		eqeq2 2833	. . . . . . . 8 ⊢ (𝑤 = 𝐷 → (𝑦 = 𝑤 ↔ 𝑦 = 𝐷))
31	30	anbi2d 630	. . . . . . 7 ⊢ (𝑤 = 𝐷 → ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) ↔ (𝑥 = 𝑧 ∧ 𝑦 = 𝐷)))
32		eqeq2 2833	. . . . . . . 8 ⊢ (𝑤 = 𝐷 → (𝑥 = 𝑤 ↔ 𝑥 = 𝐷))
33	32	anbi1d 631	. . . . . . 7 ⊢ (𝑤 = 𝐷 → ((𝑥 = 𝑤 ∧ 𝑦 = 𝑧) ↔ (𝑥 = 𝐷 ∧ 𝑦 = 𝑧)))
34	31, 33	orbi12d 915	. . . . . 6 ⊢ (𝑤 = 𝐷 → (((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) ∨ (𝑥 = 𝑤 ∧ 𝑦 = 𝑧)) ↔ ((𝑥 = 𝑧 ∧ 𝑦 = 𝐷) ∨ (𝑥 = 𝐷 ∧ 𝑦 = 𝑧))))
35		vex 3497	. . . . . . 7 ⊢ 𝑥 ∈ V
36		vex 3497	. . . . . . 7 ⊢ 𝑦 ∈ V
37		vex 3497	. . . . . . 7 ⊢ 𝑧 ∈ V
38		vex 3497	. . . . . . 7 ⊢ 𝑤 ∈ V
39	35, 36, 37, 38	preq12b 4781	. . . . . 6 ⊢ ({𝑥, 𝑦} = {𝑧, 𝑤} ↔ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) ∨ (𝑥 = 𝑤 ∧ 𝑦 = 𝑧)))
40	29, 34, 39	vtoclbg 3569	. . . . 5 ⊢ (𝐷 ∈ 𝑌 → ({𝑥, 𝑦} = {𝑧, 𝐷} ↔ ((𝑥 = 𝑧 ∧ 𝑦 = 𝐷) ∨ (𝑥 = 𝐷 ∧ 𝑦 = 𝑧))))
41	40	a1i 11	. . . 4 ⊢ ((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑊 ∧ 𝑧 ∈ 𝑋) → (𝐷 ∈ 𝑌 → ({𝑥, 𝑦} = {𝑧, 𝐷} ↔ ((𝑥 = 𝑧 ∧ 𝑦 = 𝐷) ∨ (𝑥 = 𝐷 ∧ 𝑦 = 𝑧)))))
42	9, 18, 27, 41	vtocl3ga 3578	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (𝐷 ∈ 𝑌 → ({𝐴, 𝐵} = {𝐶, 𝐷} ↔ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) ∨ (𝐴 = 𝐷 ∧ 𝐵 = 𝐶)))))
43	42	3expa 1114	. 2 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ 𝐶 ∈ 𝑋) → (𝐷 ∈ 𝑌 → ({𝐴, 𝐵} = {𝐶, 𝐷} ↔ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) ∨ (𝐴 = 𝐷 ∧ 𝐵 = 𝐶)))))
44	43	impr 457	1 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ (𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌)) → ({𝐴, 𝐵} = {𝐶, 𝐷} ↔ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) ∨ (𝐴 = 𝐷 ∧ 𝐵 = 𝐶))))

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398   ∨ wo 843   ∧ w3a 1083   = wceq 1537   ∈ wcel 2114  {cpr 4569

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-v 3496  df-un 3941  df-sn 4568  df-pr 4570

This theorem is referenced by:  prneimg  4785  pr1eqbg  4787  preqsnd  4789  preq12nebg  4793  opthprneg  4795  preleqALT  9080  pythagtriplem2  16154  pythagtrip  16171  upgrpredgv  26924  uhgr2edg  26990  usgredg2v  27009  2pthon3v  27722  opprb  43286  or2expropbi  43289  ich2exprop  43653  prsprel  43669  paireqne  43693  poprelb  43706