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
and then        , as proven in brcnv 5014
(see df-br 4173 and df-rel 4844 for more on relations). For example,
   
        
     
(ex-cnv 21698). 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 "to the
minus
one." "Converse" is Quine's terminology; some authors
call it
"inverse," especially when the argument is a function.
(Contributed by
NM, 4-Jul-1994.) |