Detailed syntax breakdown of Definition df-trs
Step | Hyp | Ref
| Expression |
1 | | ctrs 37520 |
. 2
class
Trs |
2 | | vx |
. . . . . . 7
setvar 𝑥 |
3 | 2 | cv 1539 |
. . . . . 6
class 𝑥 |
4 | 3 | cdm 5676 |
. . . . . . 7
class dom 𝑥 |
5 | 3 | crn 5677 |
. . . . . . 7
class ran 𝑥 |
6 | 4, 5 | cxp 5674 |
. . . . . 6
class (dom
𝑥 × ran 𝑥) |
7 | 3, 6 | cin 3947 |
. . . . 5
class (𝑥 ∩ (dom 𝑥 × ran 𝑥)) |
8 | 7, 7 | ccom 5680 |
. . . 4
class ((𝑥 ∩ (dom 𝑥 × ran 𝑥)) ∘ (𝑥 ∩ (dom 𝑥 × ran 𝑥))) |
9 | | cssr 37510 |
. . . 4
class
S |
10 | 8, 7, 9 | wbr 5148 |
. . 3
wff ((𝑥 ∩ (dom 𝑥 × ran 𝑥)) ∘ (𝑥 ∩ (dom 𝑥 × ran 𝑥))) S (𝑥 ∩ (dom 𝑥 × ran 𝑥)) |
11 | 10, 2 | cab 2708 |
. 2
class {𝑥 ∣ ((𝑥 ∩ (dom 𝑥 × ran 𝑥)) ∘ (𝑥 ∩ (dom 𝑥 × ran 𝑥))) S (𝑥 ∩ (dom 𝑥 × ran 𝑥))} |
12 | 1, 11 | wceq 1540 |
1
wff Trs =
{𝑥 ∣ ((𝑥 ∩ (dom 𝑥 × ran 𝑥)) ∘ (𝑥 ∩ (dom 𝑥 × ran 𝑥))) S (𝑥 ∩ (dom 𝑥 × ran 𝑥))} |