Definition df-cnv

Description: Define the converse of a class. Definition 9.12 of Quine p. 64. The converse of a binary relation swaps its arguments, i.e., if A e.V and B e. V then ( A`' R B <-> B R A ) , as proven in brcnv (see df-br and df-rel for more on relations). For example, ``' { <. 2 , 6 >. , <. 3 , 9 >. } = { <. 6 , 2 >. , <. 9 , 3 >. } ` ( ex-cnv ).

We use Quine's breve accent (smile) notation. Like Quine, we use it as a prefix, which eliminates the need for parentheses. "Converse" is Quine's terminology. Some authors use a "minus one" exponent and call it "inverse", especially when the argument is a function, although this is not in general a genuine inverse. (Contributed by NM, 4-Jul-1994)

	Ref	Expression
Assertion	df-cnv	⊢ ◡ 𝐴 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑦 𝐴 𝑥 }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	⊢ 𝐴
1	0	ccnv	⊢ ◡ 𝐴
2		vx	⊢ 𝑥
3		vy	⊢ 𝑦
4	3	cv	⊢ 𝑦
5	2	cv	⊢ 𝑥
6	4 5 0	wbr	⊢ 𝑦 𝐴 𝑥
7	6 2 3	copab	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑦 𝐴 𝑥 }
8	1 7	wceq	⊢ ◡ 𝐴 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑦 𝐴 𝑥 }