Definition df-cnv3

Description: Define a function that returns the third converse of a set. The third converse of a set takes all ordered triples in the set and swaps the second and third arguments. Based on Definition 14.1(2) of TakeutiZaring p. 143. (Contributed by BTernaryTau, 2-Sep-2026)

	Ref	Expression
Assertion	df-cnv3	Could not format assertion : No typesetting found for |- Cnv3 = ( w e. _V |-> { <. <. x , y >. , z >. | <. <. x , z >. , y >. e. w } ) with typecode |-

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ccnv3	Could not format Cnv3 : No typesetting found for class Cnv3 with typecode class
1		vw	$$setvarw$$
2		cvv	$$class\mathrm{V}$$
3		vx	$$setvarx$$
4		vy	$$setvary$$
5		vz	$$setvarz$$
6	3	cv	$$setvarx$$
7	5	cv	$$setvarz$$
8	6 7	cop	$$class⟨x,z⟩$$
9	4	cv	$$setvary$$
10	8 9	cop	$$class⟨⟨x,z⟩,y⟩$$
11	1	cv	$$setvarw$$
12	10 11	wcel	$$wff⟨⟨x,z⟩,y⟩\in w$$
13	12 3 4 5	coprab	$$class\left\{⟨⟨x,y⟩,z⟩|⟨⟨x,z⟩,y⟩\in w\right\}$$
14	1 2 13	cmpt	$$class\left(w\in \mathrm{V}⟼\left\{⟨⟨x,y⟩,z⟩|⟨⟨x,z⟩,y⟩\in w\right\}\right)$$
15	0 14	wceq	Could not format Cnv3 = ( w e. _V |-> { <. <. x , y >. , z >. | <. <. x , z >. , y >. e. w } ) : No typesetting found for wff Cnv3 = ( w e. _V |-> { <. <. x , y >. , z >. | <. <. x , z >. , y >. e. w } ) with typecode wff