Definition df-cnv 2426

Description: Define the converse of a class. Definition 9.12 of [Quine] p. 64. We use Quine's breve accent (smile) notation; as a prefix, it eliminates parentheses for us. Many authors use the postfix superscript "to the minus one".

Assertion

Ref	Expression
df-cnv	⊢ ◡A = {⟨x, y⟩∣yAx}

Distinct variable group(s):   x,y,A

Detailed syntax breakdown of Definition df-cnv

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2	1	ccnv 2409	. 2 class ◡A
3		vy	. . . . 5 set y
4	3	cv 1089	. . . 4 class y
5		vx	. . . . 5 set x
6	5	cv 1089	. . . 4 class x
7	4, 6, 1	wbr 2054	. . 3 wff yAx
8	7, 5, 3	copab 2055	. 2 class {⟨x, y⟩∣yAx}
9	2, 8	wceq 1091	1 wff ◡A = {⟨x, y⟩∣yAx}

This definition is referenced by:  cnvss 2512  elcnv 2514  opelcnvg 2517  cnvco 2520  relcnv 2624  cnvsym 2626

metamath.org