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>. | E.zE.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 E.w(x = <.z, w>. /\ y = <.w, z>.)
16	15, 4	wex 1541	. . 3 wff E.zE.w(x = <.z, w>. /\ y = <.w, z>.)
17	16, 2, 10	copab 4623	. 2 class {<.x, y>. | E.zE.w(x = <.z, w>. /\ y = <.w, z>.)}
18	1, 17	wceq 1642	1 wff Swap = {<.x, y>. | E.zE.w(x = <.z, w>. /\ y = <.w, z>.)}

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