Definition df-swap 4725

Description: Define a function that swaps the two elements of an ordered pair. (Contributed by SF, 5-Jan-2015.)

Assertion

Ref	Expression
df-swap	⊢ Swap = {⟨x, y⟩ ∣ ∃z∃w(x = ⟨z, w⟩ ∧ y = ⟨w, z⟩)}

Distinct variable group:   x,y,z,w

Detailed syntax breakdown of Definition df-swap

Step	Hyp	Ref	Expression
1		cswap 4719	. 2 class Swap
2		vx	. . . . . . . 8 setvar x
3	2	cv 1641	. . . . . . 7 class x
4		vz	. . . . . . . . 9 setvar z
5	4	cv 1641	. . . . . . . 8 class z
6		vw	. . . . . . . . 9 setvar w
7	6	cv 1641	. . . . . . . 8 class w
8	5, 7	cop 4562	. . . . . . 7 class ⟨z, w⟩
9	3, 8	wceq 1642	. . . . . 6 wff x = ⟨z, w⟩
10		vy	. . . . . . . 8 setvar y
11	10	cv 1641	. . . . . . 7 class y
12	7, 5	cop 4562	. . . . . . 7 class ⟨w, z⟩
13	11, 12	wceq 1642	. . . . . 6 wff y = ⟨w, z⟩
14	9, 13	wa 358	. . . . 5 wff (x = ⟨z, w⟩ ∧ y = ⟨w, z⟩)
15	14, 6	wex 1541	. . . 4 wff ∃w(x = ⟨z, w⟩ ∧ y = ⟨w, z⟩)
16	15, 4	wex 1541	. . 3 wff ∃z∃w(x = ⟨z, w⟩ ∧ y = ⟨w, z⟩)
17	16, 2, 10	copab 4623	. 2 class {⟨x, y⟩ ∣ ∃z∃w(x = ⟨z, w⟩ ∧ y = ⟨w, z⟩)}
18	1, 17	wceq 1642	1 wff Swap = {⟨x, y⟩ ∣ ∃z∃w(x = ⟨z, w⟩ ∧ y = ⟨w, z⟩)}

This definition is used by:  elswap  4741  brswap2  4861  brswap  5510  dfswap3  5729