Theorem preq12bg 4129

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

Assertion

Ref	Expression
preq12bg	⊢ (((A ∈ V ∧ B ∈ W) ∧ (C ∈ X ∧ D ∈ Y)) → ({A, B} = {C, D} ↔ ((A = C ∧ B = D) ∨ (A = D ∧ B = C))))

Proof of Theorem preq12bg

Dummy variables x y z w are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		preq1 3800	. . . . . . 7 ⊢ (x = A → {x, y} = {A, y})
2	1	eqeq1d 2361	. . . . . 6 ⊢ (x = A → ({x, y} = {z, D} ↔ {A, y} = {z, D}))
3		eqeq1 2359	. . . . . . . 8 ⊢ (x = A → (x = z ↔ A = z))
4	3	anbi1d 685	. . . . . . 7 ⊢ (x = A → ((x = z ∧ y = D) ↔ (A = z ∧ y = D)))
5		eqeq1 2359	. . . . . . . 8 ⊢ (x = A → (x = D ↔ A = D))
6	5	anbi1d 685	. . . . . . 7 ⊢ (x = A → ((x = D ∧ y = z) ↔ (A = D ∧ y = z)))
7	4, 6	orbi12d 690	. . . . . 6 ⊢ (x = A → (((x = z ∧ y = D) ∨ (x = D ∧ y = z)) ↔ ((A = z ∧ y = D) ∨ (A = D ∧ y = z))))
8	2, 7	bibi12d 312	. . . . 5 ⊢ (x = A → (({x, y} = {z, D} ↔ ((x = z ∧ y = D) ∨ (x = D ∧ y = z))) ↔ ({A, y} = {z, D} ↔ ((A = z ∧ y = D) ∨ (A = D ∧ y = z)))))
9	8	imbi2d 307	. . . 4 ⊢ (x = A → ((D ∈ Y → ({x, y} = {z, D} ↔ ((x = z ∧ y = D) ∨ (x = D ∧ y = z)))) ↔ (D ∈ Y → ({A, y} = {z, D} ↔ ((A = z ∧ y = D) ∨ (A = D ∧ y = z))))))
10		preq2 3801	. . . . . . 7 ⊢ (y = B → {A, y} = {A, B})
11	10	eqeq1d 2361	. . . . . 6 ⊢ (y = B → ({A, y} = {z, D} ↔ {A, B} = {z, D}))
12		eqeq1 2359	. . . . . . . 8 ⊢ (y = B → (y = D ↔ B = D))
13	12	anbi2d 684	. . . . . . 7 ⊢ (y = B → ((A = z ∧ y = D) ↔ (A = z ∧ B = D)))
14		eqeq1 2359	. . . . . . . 8 ⊢ (y = B → (y = z ↔ B = z))
15	14	anbi2d 684	. . . . . . 7 ⊢ (y = B → ((A = D ∧ y = z) ↔ (A = D ∧ B = z)))
16	13, 15	orbi12d 690	. . . . . 6 ⊢ (y = B → (((A = z ∧ y = D) ∨ (A = D ∧ y = z)) ↔ ((A = z ∧ B = D) ∨ (A = D ∧ B = z))))
17	11, 16	bibi12d 312	. . . . 5 ⊢ (y = B → (({A, y} = {z, D} ↔ ((A = z ∧ y = D) ∨ (A = D ∧ y = z))) ↔ ({A, B} = {z, D} ↔ ((A = z ∧ B = D) ∨ (A = D ∧ B = z)))))
18	17	imbi2d 307	. . . 4 ⊢ (y = B → ((D ∈ Y → ({A, y} = {z, D} ↔ ((A = z ∧ y = D) ∨ (A = D ∧ y = z)))) ↔ (D ∈ Y → ({A, B} = {z, D} ↔ ((A = z ∧ B = D) ∨ (A = D ∧ B = z))))))
19		preq1 3800	. . . . . . 7 ⊢ (z = C → {z, D} = {C, D})
20	19	eqeq2d 2364	. . . . . 6 ⊢ (z = C → ({A, B} = {z, D} ↔ {A, B} = {C, D}))
21		eqeq2 2362	. . . . . . . 8 ⊢ (z = C → (A = z ↔ A = C))
22	21	anbi1d 685	. . . . . . 7 ⊢ (z = C → ((A = z ∧ B = D) ↔ (A = C ∧ B = D)))
23		eqeq2 2362	. . . . . . . 8 ⊢ (z = C → (B = z ↔ B = C))
24	23	anbi2d 684	. . . . . . 7 ⊢ (z = C → ((A = D ∧ B = z) ↔ (A = D ∧ B = C)))
25	22, 24	orbi12d 690	. . . . . 6 ⊢ (z = C → (((A = z ∧ B = D) ∨ (A = D ∧ B = z)) ↔ ((A = C ∧ B = D) ∨ (A = D ∧ B = C))))
26	20, 25	bibi12d 312	. . . . 5 ⊢ (z = C → (({A, B} = {z, D} ↔ ((A = z ∧ B = D) ∨ (A = D ∧ B = z))) ↔ ({A, B} = {C, D} ↔ ((A = C ∧ B = D) ∨ (A = D ∧ B = C)))))
27	26	imbi2d 307	. . . 4 ⊢ (z = C → ((D ∈ Y → ({A, B} = {z, D} ↔ ((A = z ∧ B = D) ∨ (A = D ∧ B = z)))) ↔ (D ∈ Y → ({A, B} = {C, D} ↔ ((A = C ∧ B = D) ∨ (A = D ∧ B = C))))))
28		preq2 3801	. . . . . . 7 ⊢ (w = D → {z, w} = {z, D})
29	28	eqeq2d 2364	. . . . . 6 ⊢ (w = D → ({x, y} = {z, w} ↔ {x, y} = {z, D}))
30		eqeq2 2362	. . . . . . . 8 ⊢ (w = D → (y = w ↔ y = D))
31	30	anbi2d 684	. . . . . . 7 ⊢ (w = D → ((x = z ∧ y = w) ↔ (x = z ∧ y = D)))
32		eqeq2 2362	. . . . . . . 8 ⊢ (w = D → (x = w ↔ x = D))
33	32	anbi1d 685	. . . . . . 7 ⊢ (w = D → ((x = w ∧ y = z) ↔ (x = D ∧ y = z)))
34	31, 33	orbi12d 690	. . . . . 6 ⊢ (w = D → (((x = z ∧ y = w) ∨ (x = w ∧ y = z)) ↔ ((x = z ∧ y = D) ∨ (x = D ∧ y = z))))
35		vex 2863	. . . . . . 7 ⊢ x ∈ V
36		vex 2863	. . . . . . 7 ⊢ y ∈ V
37		vex 2863	. . . . . . 7 ⊢ z ∈ V
38		vex 2863	. . . . . . 7 ⊢ w ∈ V
39	35, 36, 37, 38	preq12b 4128	. . . . . 6 ⊢ ({x, y} = {z, w} ↔ ((x = z ∧ y = w) ∨ (x = w ∧ y = z)))
40	29, 34, 39	vtoclbg 2916	. . . . 5 ⊢ (D ∈ Y → ({x, y} = {z, D} ↔ ((x = z ∧ y = D) ∨ (x = D ∧ y = z))))
41	40	a1i 10	. . . 4 ⊢ ((x ∈ V ∧ y ∈ W ∧ z ∈ X) → (D ∈ Y → ({x, y} = {z, D} ↔ ((x = z ∧ y = D) ∨ (x = D ∧ y = z)))))
42	9, 18, 27, 41	vtocl3ga 2925	. . 3 ⊢ ((A ∈ V ∧ B ∈ W ∧ C ∈ X) → (D ∈ Y → ({A, B} = {C, D} ↔ ((A = C ∧ B = D) ∨ (A = D ∧ B = C)))))
43	42	3expa 1151	. 2 ⊢ (((A ∈ V ∧ B ∈ W) ∧ C ∈ X) → (D ∈ Y → ({A, B} = {C, D} ↔ ((A = C ∧ B = D) ∨ (A = D ∧ B = C)))))
44	43	impr 602	1 ⊢ (((A ∈ V ∧ B ∈ W) ∧ (C ∈ X ∧ D ∈ Y)) → ({A, B} = {C, D} ↔ ((A = C ∧ B = D) ∨ (A = D ∧ B = C))))

Syntax hints:   → wi 4   ↔ wb 176   ∨ wo 357   ∧ wa 358   ∧ w3a 934   = wceq 1642   ∈ wcel 1710  {cpr 3739

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925  ax-ext 2334

This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-nan 1288  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2340  df-cleq 2346  df-clel 2349  df-nfc 2479  df-v 2862  df-nin 3212  df-compl 3213  df-un 3215  df-sn 3742  df-pr 3743

This theorem is referenced by: (None)