Theorem preq12bg 4129

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

Assertion

Ref	Expression
preq12bg	|- (((A e. V /\ B e. W) /\ (C e. X /\ D e. 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 e. Y -> ({x, y} = {z, D} <-> ((x = z /\ y = D) \/ (x = D /\ y = z)))) <-> (D e. 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 e. Y -> ({A, y} = {z, D} <-> ((A = z /\ y = D) \/ (A = D /\ y = z)))) <-> (D e. 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 e. Y -> ({A, B} = {z, D} <-> ((A = z /\ B = D) \/ (A = D /\ B = z)))) <-> (D e. 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 e. _V
36		vex 2863	. . . . . . 7 |- y e. _V
37		vex 2863	. . . . . . 7 |- z e. _V
38		vex 2863	. . . . . . 7 |- w e. _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 e. Y -> ({x, y} = {z, D} <-> ((x = z /\ y = D) \/ (x = D /\ y = z))))
41	40	a1i 10	. . . 4 |- ((x e. V /\ y e. W /\ z e. X) -> (D e. Y -> ({x, y} = {z, D} <-> ((x = z /\ y = D) \/ (x = D /\ y = z)))))
42	9, 18, 27, 41	vtocl3ga 2925	. . 3 |- ((A e. V /\ B e. W /\ C e. X) -> (D e. Y -> ({A, B} = {C, D} <-> ((A = C /\ B = D) \/ (A = D /\ B = C)))))
43	42	3expa 1151	. 2 |- (((A e. V /\ B e. W) /\ C e. X) -> (D e. Y -> ({A, B} = {C, D} <-> ((A = C /\ B = D) \/ (A = D /\ B = C)))))
44	43	impr 602	1 |- (((A e. V /\ B e. W) /\ (C e. X /\ D e. 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   e. 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)