![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > df-cnv | 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 4810
(see df-br 4004 and df-rel 4633 for more on relations). For example,
◡{〈2,
6〉, 〈3, 9〉} = {〈6, 2〉, 〈9, 3〉}.
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 4625 | . 2 class ◡𝐴 |
3 | vy | . . . . 5 setvar 𝑦 | |
4 | 3 | cv 1352 | . . . 4 class 𝑦 |
5 | vx | . . . . 5 setvar 𝑥 | |
6 | 5 | cv 1352 | . . . 4 class 𝑥 |
7 | 4, 6, 1 | wbr 4003 | . . 3 wff 𝑦𝐴𝑥 |
8 | 7, 5, 3 | copab 4063 | . 2 class {〈𝑥, 𝑦〉 ∣ 𝑦𝐴𝑥} |
9 | 2, 8 | wceq 1353 | 1 wff ◡𝐴 = {〈𝑥, 𝑦〉 ∣ 𝑦𝐴𝑥} |
Colors of variables: wff set class |
This definition is referenced by: cnvss 4800 elcnv 4804 nfcnv 4806 opelcnvg 4807 csbcnvg 4811 cnvco 4812 relcnv 5006 cnvi 5033 cnvun 5034 cnvin 5036 cnvcnv3 5078 |
Copyright terms: Public domain | W3C validator |