Theorem preq12bg 4789

Description: Closed form of preq12b 4786. (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 4674	. . . . . . 7 ⊢ (𝑥 = 𝐴 → {𝑥, 𝑦} = {𝐴, 𝑦})
2	1	eqeq1d 2741	. . . . . 6 ⊢ (𝑥 = 𝐴 → ({𝑥, 𝑦} = {𝑧, 𝐷} ↔ {𝐴, 𝑦} = {𝑧, 𝐷}))
3		eqeq1 2743	. . . . . . . 8 ⊢ (𝑥 = 𝐴 → (𝑥 = 𝑧 ↔ 𝐴 = 𝑧))
4	3	anbi1d 629	. . . . . . 7 ⊢ (𝑥 = 𝐴 → ((𝑥 = 𝑧 ∧ 𝑦 = 𝐷) ↔ (𝐴 = 𝑧 ∧ 𝑦 = 𝐷)))
5		eqeq1 2743	. . . . . . . 8 ⊢ (𝑥 = 𝐴 → (𝑥 = 𝐷 ↔ 𝐴 = 𝐷))
6	5	anbi1d 629	. . . . . . 7 ⊢ (𝑥 = 𝐴 → ((𝑥 = 𝐷 ∧ 𝑦 = 𝑧) ↔ (𝐴 = 𝐷 ∧ 𝑦 = 𝑧)))
7	4, 6	orbi12d 915	. . . . . 6 ⊢ (𝑥 = 𝐴 → (((𝑥 = 𝑧 ∧ 𝑦 = 𝐷) ∨ (𝑥 = 𝐷 ∧ 𝑦 = 𝑧)) ↔ ((𝐴 = 𝑧 ∧ 𝑦 = 𝐷) ∨ (𝐴 = 𝐷 ∧ 𝑦 = 𝑧))))
8	2, 7	bibi12d 345	. . . . 5 ⊢ (𝑥 = 𝐴 → (({𝑥, 𝑦} = {𝑧, 𝐷} ↔ ((𝑥 = 𝑧 ∧ 𝑦 = 𝐷) ∨ (𝑥 = 𝐷 ∧ 𝑦 = 𝑧))) ↔ ({𝐴, 𝑦} = {𝑧, 𝐷} ↔ ((𝐴 = 𝑧 ∧ 𝑦 = 𝐷) ∨ (𝐴 = 𝐷 ∧ 𝑦 = 𝑧)))))
9	8	imbi2d 340	. . . 4 ⊢ (𝑥 = 𝐴 → ((𝐷 ∈ 𝑌 → ({𝑥, 𝑦} = {𝑧, 𝐷} ↔ ((𝑥 = 𝑧 ∧ 𝑦 = 𝐷) ∨ (𝑥 = 𝐷 ∧ 𝑦 = 𝑧)))) ↔ (𝐷 ∈ 𝑌 → ({𝐴, 𝑦} = {𝑧, 𝐷} ↔ ((𝐴 = 𝑧 ∧ 𝑦 = 𝐷) ∨ (𝐴 = 𝐷 ∧ 𝑦 = 𝑧))))))
10		preq2 4675	. . . . . . 7 ⊢ (𝑦 = 𝐵 → {𝐴, 𝑦} = {𝐴, 𝐵})
11	10	eqeq1d 2741	. . . . . 6 ⊢ (𝑦 = 𝐵 → ({𝐴, 𝑦} = {𝑧, 𝐷} ↔ {𝐴, 𝐵} = {𝑧, 𝐷}))
12		eqeq1 2743	. . . . . . . 8 ⊢ (𝑦 = 𝐵 → (𝑦 = 𝐷 ↔ 𝐵 = 𝐷))
13	12	anbi2d 628	. . . . . . 7 ⊢ (𝑦 = 𝐵 → ((𝐴 = 𝑧 ∧ 𝑦 = 𝐷) ↔ (𝐴 = 𝑧 ∧ 𝐵 = 𝐷)))
14		eqeq1 2743	. . . . . . . 8 ⊢ (𝑦 = 𝐵 → (𝑦 = 𝑧 ↔ 𝐵 = 𝑧))
15	14	anbi2d 628	. . . . . . 7 ⊢ (𝑦 = 𝐵 → ((𝐴 = 𝐷 ∧ 𝑦 = 𝑧) ↔ (𝐴 = 𝐷 ∧ 𝐵 = 𝑧)))
16	13, 15	orbi12d 915	. . . . . 6 ⊢ (𝑦 = 𝐵 → (((𝐴 = 𝑧 ∧ 𝑦 = 𝐷) ∨ (𝐴 = 𝐷 ∧ 𝑦 = 𝑧)) ↔ ((𝐴 = 𝑧 ∧ 𝐵 = 𝐷) ∨ (𝐴 = 𝐷 ∧ 𝐵 = 𝑧))))
17	11, 16	bibi12d 345	. . . . 5 ⊢ (𝑦 = 𝐵 → (({𝐴, 𝑦} = {𝑧, 𝐷} ↔ ((𝐴 = 𝑧 ∧ 𝑦 = 𝐷) ∨ (𝐴 = 𝐷 ∧ 𝑦 = 𝑧))) ↔ ({𝐴, 𝐵} = {𝑧, 𝐷} ↔ ((𝐴 = 𝑧 ∧ 𝐵 = 𝐷) ∨ (𝐴 = 𝐷 ∧ 𝐵 = 𝑧)))))
18	17	imbi2d 340	. . . 4 ⊢ (𝑦 = 𝐵 → ((𝐷 ∈ 𝑌 → ({𝐴, 𝑦} = {𝑧, 𝐷} ↔ ((𝐴 = 𝑧 ∧ 𝑦 = 𝐷) ∨ (𝐴 = 𝐷 ∧ 𝑦 = 𝑧)))) ↔ (𝐷 ∈ 𝑌 → ({𝐴, 𝐵} = {𝑧, 𝐷} ↔ ((𝐴 = 𝑧 ∧ 𝐵 = 𝐷) ∨ (𝐴 = 𝐷 ∧ 𝐵 = 𝑧))))))
19		preq1 4674	. . . . . . 7 ⊢ (𝑧 = 𝐶 → {𝑧, 𝐷} = {𝐶, 𝐷})
20	19	eqeq2d 2750	. . . . . 6 ⊢ (𝑧 = 𝐶 → ({𝐴, 𝐵} = {𝑧, 𝐷} ↔ {𝐴, 𝐵} = {𝐶, 𝐷}))
21		eqeq2 2751	. . . . . . . 8 ⊢ (𝑧 = 𝐶 → (𝐴 = 𝑧 ↔ 𝐴 = 𝐶))
22	21	anbi1d 629	. . . . . . 7 ⊢ (𝑧 = 𝐶 → ((𝐴 = 𝑧 ∧ 𝐵 = 𝐷) ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷)))
23		eqeq2 2751	. . . . . . . 8 ⊢ (𝑧 = 𝐶 → (𝐵 = 𝑧 ↔ 𝐵 = 𝐶))
24	23	anbi2d 628	. . . . . . 7 ⊢ (𝑧 = 𝐶 → ((𝐴 = 𝐷 ∧ 𝐵 = 𝑧) ↔ (𝐴 = 𝐷 ∧ 𝐵 = 𝐶)))
25	22, 24	orbi12d 915	. . . . . 6 ⊢ (𝑧 = 𝐶 → (((𝐴 = 𝑧 ∧ 𝐵 = 𝐷) ∨ (𝐴 = 𝐷 ∧ 𝐵 = 𝑧)) ↔ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) ∨ (𝐴 = 𝐷 ∧ 𝐵 = 𝐶))))
26	20, 25	bibi12d 345	. . . . 5 ⊢ (𝑧 = 𝐶 → (({𝐴, 𝐵} = {𝑧, 𝐷} ↔ ((𝐴 = 𝑧 ∧ 𝐵 = 𝐷) ∨ (𝐴 = 𝐷 ∧ 𝐵 = 𝑧))) ↔ ({𝐴, 𝐵} = {𝐶, 𝐷} ↔ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) ∨ (𝐴 = 𝐷 ∧ 𝐵 = 𝐶)))))
27	26	imbi2d 340	. . . 4 ⊢ (𝑧 = 𝐶 → ((𝐷 ∈ 𝑌 → ({𝐴, 𝐵} = {𝑧, 𝐷} ↔ ((𝐴 = 𝑧 ∧ 𝐵 = 𝐷) ∨ (𝐴 = 𝐷 ∧ 𝐵 = 𝑧)))) ↔ (𝐷 ∈ 𝑌 → ({𝐴, 𝐵} = {𝐶, 𝐷} ↔ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) ∨ (𝐴 = 𝐷 ∧ 𝐵 = 𝐶))))))
28		preq2 4675	. . . . . . 7 ⊢ (𝑤 = 𝐷 → {𝑧, 𝑤} = {𝑧, 𝐷})
29	28	eqeq2d 2750	. . . . . 6 ⊢ (𝑤 = 𝐷 → ({𝑥, 𝑦} = {𝑧, 𝑤} ↔ {𝑥, 𝑦} = {𝑧, 𝐷}))
30		eqeq2 2751	. . . . . . . 8 ⊢ (𝑤 = 𝐷 → (𝑦 = 𝑤 ↔ 𝑦 = 𝐷))
31	30	anbi2d 628	. . . . . . 7 ⊢ (𝑤 = 𝐷 → ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) ↔ (𝑥 = 𝑧 ∧ 𝑦 = 𝐷)))
32		eqeq2 2751	. . . . . . . 8 ⊢ (𝑤 = 𝐷 → (𝑥 = 𝑤 ↔ 𝑥 = 𝐷))
33	32	anbi1d 629	. . . . . . 7 ⊢ (𝑤 = 𝐷 → ((𝑥 = 𝑤 ∧ 𝑦 = 𝑧) ↔ (𝑥 = 𝐷 ∧ 𝑦 = 𝑧)))
34	31, 33	orbi12d 915	. . . . . 6 ⊢ (𝑤 = 𝐷 → (((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) ∨ (𝑥 = 𝑤 ∧ 𝑦 = 𝑧)) ↔ ((𝑥 = 𝑧 ∧ 𝑦 = 𝐷) ∨ (𝑥 = 𝐷 ∧ 𝑦 = 𝑧))))
35		vex 3434	. . . . . . 7 ⊢ 𝑥 ∈ V
36		vex 3434	. . . . . . 7 ⊢ 𝑦 ∈ V
37		vex 3434	. . . . . . 7 ⊢ 𝑧 ∈ V
38		vex 3434	. . . . . . 7 ⊢ 𝑤 ∈ V
39	35, 36, 37, 38	preq12b 4786	. . . . . 6 ⊢ ({𝑥, 𝑦} = {𝑧, 𝑤} ↔ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) ∨ (𝑥 = 𝑤 ∧ 𝑦 = 𝑧)))
40	29, 34, 39	vtoclbg 3505	. . . . 5 ⊢ (𝐷 ∈ 𝑌 → ({𝑥, 𝑦} = {𝑧, 𝐷} ↔ ((𝑥 = 𝑧 ∧ 𝑦 = 𝐷) ∨ (𝑥 = 𝐷 ∧ 𝑦 = 𝑧))))
41	40	a1i 11	. . . 4 ⊢ ((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑊 ∧ 𝑧 ∈ 𝑋) → (𝐷 ∈ 𝑌 → ({𝑥, 𝑦} = {𝑧, 𝐷} ↔ ((𝑥 = 𝑧 ∧ 𝑦 = 𝐷) ∨ (𝑥 = 𝐷 ∧ 𝑦 = 𝑧)))))
42	9, 18, 27, 41	vtocl3ga 3515	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (𝐷 ∈ 𝑌 → ({𝐴, 𝐵} = {𝐶, 𝐷} ↔ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) ∨ (𝐴 = 𝐷 ∧ 𝐵 = 𝐶)))))
43	42	3expa 1116	. 2 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ 𝐶 ∈ 𝑋) → (𝐷 ∈ 𝑌 → ({𝐴, 𝐵} = {𝐶, 𝐷} ↔ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) ∨ (𝐴 = 𝐷 ∧ 𝐵 = 𝐶)))))
44	43	impr 454	1 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ (𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌)) → ({𝐴, 𝐵} = {𝐶, 𝐷} ↔ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) ∨ (𝐴 = 𝐷 ∧ 𝐵 = 𝐶))))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395   ∨ wo 843   ∧ w3a 1085   = wceq 1541   ∈ wcel 2109  {cpr 4568

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1544  df-ex 1786  df-sb 2071  df-clab 2717  df-cleq 2731  df-clel 2817  df-v 3432  df-un 3896  df-sn 4567  df-pr 4569

This theorem is referenced by:  prneimg  4790  pr1eqbg  4792  preqsnd  4794  preq12nebg  4798  opthprneg  4800  preleqALT  9336  pythagtriplem2  16499  pythagtrip  16516  upgrpredgv  27490  uhgr2edg  27556  usgredg2v  27575  2pthon3v  28287  opprb  44476  or2expropbi  44479  ich2exprop  44875  prsprel  44891  paireqne  44915  poprelb  44928