Theorem preq12bg 4855

Description: Closed form of preq12b 4852. (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 4738	. . . . . . 7 ⊢ (𝑥 = 𝐴 → {𝑥, 𝑦} = {𝐴, 𝑦})
2	1	eqeq1d 2735	. . . . . 6 ⊢ (𝑥 = 𝐴 → ({𝑥, 𝑦} = {𝑧, 𝐷} ↔ {𝐴, 𝑦} = {𝑧, 𝐷}))
3		eqeq1 2737	. . . . . . . 8 ⊢ (𝑥 = 𝐴 → (𝑥 = 𝑧 ↔ 𝐴 = 𝑧))
4	3	anbi1d 631	. . . . . . 7 ⊢ (𝑥 = 𝐴 → ((𝑥 = 𝑧 ∧ 𝑦 = 𝐷) ↔ (𝐴 = 𝑧 ∧ 𝑦 = 𝐷)))
5		eqeq1 2737	. . . . . . . 8 ⊢ (𝑥 = 𝐴 → (𝑥 = 𝐷 ↔ 𝐴 = 𝐷))
6	5	anbi1d 631	. . . . . . 7 ⊢ (𝑥 = 𝐴 → ((𝑥 = 𝐷 ∧ 𝑦 = 𝑧) ↔ (𝐴 = 𝐷 ∧ 𝑦 = 𝑧)))
7	4, 6	orbi12d 918	. . . . . 6 ⊢ (𝑥 = 𝐴 → (((𝑥 = 𝑧 ∧ 𝑦 = 𝐷) ∨ (𝑥 = 𝐷 ∧ 𝑦 = 𝑧)) ↔ ((𝐴 = 𝑧 ∧ 𝑦 = 𝐷) ∨ (𝐴 = 𝐷 ∧ 𝑦 = 𝑧))))
8	2, 7	bibi12d 346	. . . . 5 ⊢ (𝑥 = 𝐴 → (({𝑥, 𝑦} = {𝑧, 𝐷} ↔ ((𝑥 = 𝑧 ∧ 𝑦 = 𝐷) ∨ (𝑥 = 𝐷 ∧ 𝑦 = 𝑧))) ↔ ({𝐴, 𝑦} = {𝑧, 𝐷} ↔ ((𝐴 = 𝑧 ∧ 𝑦 = 𝐷) ∨ (𝐴 = 𝐷 ∧ 𝑦 = 𝑧)))))
9	8	imbi2d 341	. . . 4 ⊢ (𝑥 = 𝐴 → ((𝐷 ∈ 𝑌 → ({𝑥, 𝑦} = {𝑧, 𝐷} ↔ ((𝑥 = 𝑧 ∧ 𝑦 = 𝐷) ∨ (𝑥 = 𝐷 ∧ 𝑦 = 𝑧)))) ↔ (𝐷 ∈ 𝑌 → ({𝐴, 𝑦} = {𝑧, 𝐷} ↔ ((𝐴 = 𝑧 ∧ 𝑦 = 𝐷) ∨ (𝐴 = 𝐷 ∧ 𝑦 = 𝑧))))))
10		preq2 4739	. . . . . . 7 ⊢ (𝑦 = 𝐵 → {𝐴, 𝑦} = {𝐴, 𝐵})
11	10	eqeq1d 2735	. . . . . 6 ⊢ (𝑦 = 𝐵 → ({𝐴, 𝑦} = {𝑧, 𝐷} ↔ {𝐴, 𝐵} = {𝑧, 𝐷}))
12		eqeq1 2737	. . . . . . . 8 ⊢ (𝑦 = 𝐵 → (𝑦 = 𝐷 ↔ 𝐵 = 𝐷))
13	12	anbi2d 630	. . . . . . 7 ⊢ (𝑦 = 𝐵 → ((𝐴 = 𝑧 ∧ 𝑦 = 𝐷) ↔ (𝐴 = 𝑧 ∧ 𝐵 = 𝐷)))
14		eqeq1 2737	. . . . . . . 8 ⊢ (𝑦 = 𝐵 → (𝑦 = 𝑧 ↔ 𝐵 = 𝑧))
15	14	anbi2d 630	. . . . . . 7 ⊢ (𝑦 = 𝐵 → ((𝐴 = 𝐷 ∧ 𝑦 = 𝑧) ↔ (𝐴 = 𝐷 ∧ 𝐵 = 𝑧)))
16	13, 15	orbi12d 918	. . . . . 6 ⊢ (𝑦 = 𝐵 → (((𝐴 = 𝑧 ∧ 𝑦 = 𝐷) ∨ (𝐴 = 𝐷 ∧ 𝑦 = 𝑧)) ↔ ((𝐴 = 𝑧 ∧ 𝐵 = 𝐷) ∨ (𝐴 = 𝐷 ∧ 𝐵 = 𝑧))))
17	11, 16	bibi12d 346	. . . . 5 ⊢ (𝑦 = 𝐵 → (({𝐴, 𝑦} = {𝑧, 𝐷} ↔ ((𝐴 = 𝑧 ∧ 𝑦 = 𝐷) ∨ (𝐴 = 𝐷 ∧ 𝑦 = 𝑧))) ↔ ({𝐴, 𝐵} = {𝑧, 𝐷} ↔ ((𝐴 = 𝑧 ∧ 𝐵 = 𝐷) ∨ (𝐴 = 𝐷 ∧ 𝐵 = 𝑧)))))
18	17	imbi2d 341	. . . 4 ⊢ (𝑦 = 𝐵 → ((𝐷 ∈ 𝑌 → ({𝐴, 𝑦} = {𝑧, 𝐷} ↔ ((𝐴 = 𝑧 ∧ 𝑦 = 𝐷) ∨ (𝐴 = 𝐷 ∧ 𝑦 = 𝑧)))) ↔ (𝐷 ∈ 𝑌 → ({𝐴, 𝐵} = {𝑧, 𝐷} ↔ ((𝐴 = 𝑧 ∧ 𝐵 = 𝐷) ∨ (𝐴 = 𝐷 ∧ 𝐵 = 𝑧))))))
19		preq1 4738	. . . . . . 7 ⊢ (𝑧 = 𝐶 → {𝑧, 𝐷} = {𝐶, 𝐷})
20	19	eqeq2d 2744	. . . . . 6 ⊢ (𝑧 = 𝐶 → ({𝐴, 𝐵} = {𝑧, 𝐷} ↔ {𝐴, 𝐵} = {𝐶, 𝐷}))
21		eqeq2 2745	. . . . . . . 8 ⊢ (𝑧 = 𝐶 → (𝐴 = 𝑧 ↔ 𝐴 = 𝐶))
22	21	anbi1d 631	. . . . . . 7 ⊢ (𝑧 = 𝐶 → ((𝐴 = 𝑧 ∧ 𝐵 = 𝐷) ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷)))
23		eqeq2 2745	. . . . . . . 8 ⊢ (𝑧 = 𝐶 → (𝐵 = 𝑧 ↔ 𝐵 = 𝐶))
24	23	anbi2d 630	. . . . . . 7 ⊢ (𝑧 = 𝐶 → ((𝐴 = 𝐷 ∧ 𝐵 = 𝑧) ↔ (𝐴 = 𝐷 ∧ 𝐵 = 𝐶)))
25	22, 24	orbi12d 918	. . . . . 6 ⊢ (𝑧 = 𝐶 → (((𝐴 = 𝑧 ∧ 𝐵 = 𝐷) ∨ (𝐴 = 𝐷 ∧ 𝐵 = 𝑧)) ↔ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) ∨ (𝐴 = 𝐷 ∧ 𝐵 = 𝐶))))
26	20, 25	bibi12d 346	. . . . 5 ⊢ (𝑧 = 𝐶 → (({𝐴, 𝐵} = {𝑧, 𝐷} ↔ ((𝐴 = 𝑧 ∧ 𝐵 = 𝐷) ∨ (𝐴 = 𝐷 ∧ 𝐵 = 𝑧))) ↔ ({𝐴, 𝐵} = {𝐶, 𝐷} ↔ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) ∨ (𝐴 = 𝐷 ∧ 𝐵 = 𝐶)))))
27	26	imbi2d 341	. . . 4 ⊢ (𝑧 = 𝐶 → ((𝐷 ∈ 𝑌 → ({𝐴, 𝐵} = {𝑧, 𝐷} ↔ ((𝐴 = 𝑧 ∧ 𝐵 = 𝐷) ∨ (𝐴 = 𝐷 ∧ 𝐵 = 𝑧)))) ↔ (𝐷 ∈ 𝑌 → ({𝐴, 𝐵} = {𝐶, 𝐷} ↔ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) ∨ (𝐴 = 𝐷 ∧ 𝐵 = 𝐶))))))
28		preq2 4739	. . . . . . 7 ⊢ (𝑤 = 𝐷 → {𝑧, 𝑤} = {𝑧, 𝐷})
29	28	eqeq2d 2744	. . . . . 6 ⊢ (𝑤 = 𝐷 → ({𝑥, 𝑦} = {𝑧, 𝑤} ↔ {𝑥, 𝑦} = {𝑧, 𝐷}))
30		eqeq2 2745	. . . . . . . 8 ⊢ (𝑤 = 𝐷 → (𝑦 = 𝑤 ↔ 𝑦 = 𝐷))
31	30	anbi2d 630	. . . . . . 7 ⊢ (𝑤 = 𝐷 → ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) ↔ (𝑥 = 𝑧 ∧ 𝑦 = 𝐷)))
32		eqeq2 2745	. . . . . . . 8 ⊢ (𝑤 = 𝐷 → (𝑥 = 𝑤 ↔ 𝑥 = 𝐷))
33	32	anbi1d 631	. . . . . . 7 ⊢ (𝑤 = 𝐷 → ((𝑥 = 𝑤 ∧ 𝑦 = 𝑧) ↔ (𝑥 = 𝐷 ∧ 𝑦 = 𝑧)))
34	31, 33	orbi12d 918	. . . . . 6 ⊢ (𝑤 = 𝐷 → (((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) ∨ (𝑥 = 𝑤 ∧ 𝑦 = 𝑧)) ↔ ((𝑥 = 𝑧 ∧ 𝑦 = 𝐷) ∨ (𝑥 = 𝐷 ∧ 𝑦 = 𝑧))))
35		vex 3479	. . . . . . 7 ⊢ 𝑥 ∈ V
36		vex 3479	. . . . . . 7 ⊢ 𝑦 ∈ V
37		vex 3479	. . . . . . 7 ⊢ 𝑧 ∈ V
38		vex 3479	. . . . . . 7 ⊢ 𝑤 ∈ V
39	35, 36, 37, 38	preq12b 4852	. . . . . 6 ⊢ ({𝑥, 𝑦} = {𝑧, 𝑤} ↔ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) ∨ (𝑥 = 𝑤 ∧ 𝑦 = 𝑧)))
40	29, 34, 39	vtoclbg 3560	. . . . 5 ⊢ (𝐷 ∈ 𝑌 → ({𝑥, 𝑦} = {𝑧, 𝐷} ↔ ((𝑥 = 𝑧 ∧ 𝑦 = 𝐷) ∨ (𝑥 = 𝐷 ∧ 𝑦 = 𝑧))))
41	40	a1i 11	. . . 4 ⊢ ((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑊 ∧ 𝑧 ∈ 𝑋) → (𝐷 ∈ 𝑌 → ({𝑥, 𝑦} = {𝑧, 𝐷} ↔ ((𝑥 = 𝑧 ∧ 𝑦 = 𝐷) ∨ (𝑥 = 𝐷 ∧ 𝑦 = 𝑧)))))
42	9, 18, 27, 41	vtocl3ga 3570	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (𝐷 ∈ 𝑌 → ({𝐴, 𝐵} = {𝐶, 𝐷} ↔ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) ∨ (𝐴 = 𝐷 ∧ 𝐵 = 𝐶)))))
43	42	3expa 1119	. 2 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ 𝐶 ∈ 𝑋) → (𝐷 ∈ 𝑌 → ({𝐴, 𝐵} = {𝐶, 𝐷} ↔ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) ∨ (𝐴 = 𝐷 ∧ 𝐵 = 𝐶)))))
44	43	impr 456	1 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ (𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌)) → ({𝐴, 𝐵} = {𝐶, 𝐷} ↔ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) ∨ (𝐴 = 𝐷 ∧ 𝐵 = 𝐶))))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 397   ∨ wo 846   ∧ w3a 1088   = wceq 1542   ∈ wcel 2107  {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-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-un 3954  df-sn 4630  df-pr 4632

This theorem is referenced by:  prneimg  4856  pr1eqbg  4858  preqsnd  4860  preq12nebg  4864  opthprneg  4866  preleqALT  9612  pythagtriplem2  16750  pythagtrip  16767  upgrpredgv  28399  uhgr2edg  28465  usgredg2v  28484  2pthon3v  29197  opprb  45741  or2expropbi  45744  ich2exprop  46139  prsprel  46155  paireqne  46179  poprelb  46192