# Metamath Proof Explorer

## 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. Many authors use the postfix superscript "minus one". The term "converse" is Quine's terminology; some authors call it "inverse", especially when the argument is a function. (Contributed by NM, 4-Jul-1994)

Ref Expression
Assertion df-cnv ${⊢}{{A}}^{-1}=\left\{⟨{x},{y}⟩|{y}{A}{x}\right\}$

### Detailed syntax breakdown

Step Hyp Ref Expression
0 cA ${class}{A}$
1 0 ccnv ${class}{{A}}^{-1}$
2 vx ${setvar}{x}$
3 vy ${setvar}{y}$
4 3 cv ${setvar}{y}$
5 2 cv ${setvar}{x}$
6 4 5 0 wbr ${wff}{y}{A}{x}$
7 6 2 3 copab ${class}\left\{⟨{x},{y}⟩|{y}{A}{x}\right\}$
8 1 7 wceq ${wff}{{A}}^{-1}=\left\{⟨{x},{y}⟩|{y}{A}{x}\right\}$