HomeRelated theorems
Unicode version
| Home |
Metamath Proof Explorer |
< Previous
Next >
Related theorems Unicode version |
| Description: Define the converse of a class. Definition 9.12 of [Quine] p. 64. 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. |
| Ref | Expression |
|---|---|
| df-cnv |
            |
,,| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | cA |
. . 3
 | |
| 2 | 1 | ccnv 3159 |
. 2
|
| 3 | vy |
. . . . 5
 | |
| 4 | 3 | cv 952 |
. . . 4
|
| 5 | vx |
. . . . 5
| |
| 6 | 5 | cv 952 |
. . . 4
|
| 7 | 4, 6, 1 | wbr 2609 |
. . 3
 |
| 8 | 7, 5, 3 | copab 2656 |
. 2
|
| 9 | 2, 8 | wceq 953 |
1
|
| Colors of variables: wff set class |
| This definition is referenced by: cnvss 3280 elcnv 3282 opelcnvg 3285 cnvco 3289 relcnv 3419 cnvsym 3421 |