| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > df-cnv | Structured version Visualization version GIF version | ||
| 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 𝐴 ∈
V
and 𝐵 ∈ V then (𝐴◡𝑅𝐵 ↔ 𝐵𝑅𝐴), as proven in brcnv 5893
(see df-br 5144 and df-rel 5692 for more on relations). For example,
◡{〈2,
6〉, 〈3, 9〉} = {〈6, 2〉, 〈9, 3〉}
(ex-cnv 30456).
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 |
|---|---|
| df-cnv | ⊢ ◡𝐴 = {〈𝑥, 𝑦〉 ∣ 𝑦𝐴𝑥} |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | cA | . . 3 class 𝐴 | |
| 2 | 1 | ccnv 5684 | . 2 class ◡𝐴 |
| 3 | vy | . . . . 5 setvar 𝑦 | |
| 4 | 3 | cv 1539 | . . . 4 class 𝑦 |
| 5 | vx | . . . . 5 setvar 𝑥 | |
| 6 | 5 | cv 1539 | . . . 4 class 𝑥 |
| 7 | 4, 6, 1 | wbr 5143 | . . 3 wff 𝑦𝐴𝑥 |
| 8 | 7, 5, 3 | copab 5205 | . 2 class {〈𝑥, 𝑦〉 ∣ 𝑦𝐴𝑥} |
| 9 | 2, 8 | wceq 1540 | 1 wff ◡𝐴 = {〈𝑥, 𝑦〉 ∣ 𝑦𝐴𝑥} |
| Colors of variables: wff setvar class |
| This definition is referenced by: cnvss 5883 elcnv 5887 nfcnv 5889 brcnvg 5890 csbcnv 5894 csbcnvgALT 5895 cnvco 5896 relcnv 6122 cnv0 6160 cnvi 6161 cnvun 6162 cnvcnv3 6208 |
| Copyright terms: Public domain | W3C validator |