Detailed syntax breakdown of Definition df-trs
Step | Hyp | Ref
| Expression |
1 | | ctrs 36346 |
. 2
class
Trs |
2 | | vx |
. . . . . . 7
setvar 𝑥 |
3 | 2 | cv 1538 |
. . . . . 6
class 𝑥 |
4 | 3 | cdm 5589 |
. . . . . . 7
class dom 𝑥 |
5 | 3 | crn 5590 |
. . . . . . 7
class ran 𝑥 |
6 | 4, 5 | cxp 5587 |
. . . . . 6
class (dom
𝑥 × ran 𝑥) |
7 | 3, 6 | cin 3886 |
. . . . 5
class (𝑥 ∩ (dom 𝑥 × ran 𝑥)) |
8 | 7, 7 | ccom 5593 |
. . . 4
class ((𝑥 ∩ (dom 𝑥 × ran 𝑥)) ∘ (𝑥 ∩ (dom 𝑥 × ran 𝑥))) |
9 | | cssr 36336 |
. . . 4
class
S |
10 | 8, 7, 9 | wbr 5074 |
. . 3
wff ((𝑥 ∩ (dom 𝑥 × ran 𝑥)) ∘ (𝑥 ∩ (dom 𝑥 × ran 𝑥))) S (𝑥 ∩ (dom 𝑥 × ran 𝑥)) |
11 | 10, 2 | cab 2715 |
. 2
class {𝑥 ∣ ((𝑥 ∩ (dom 𝑥 × ran 𝑥)) ∘ (𝑥 ∩ (dom 𝑥 × ran 𝑥))) S (𝑥 ∩ (dom 𝑥 × ran 𝑥))} |
12 | 1, 11 | wceq 1539 |
1
wff Trs =
{𝑥 ∣ ((𝑥 ∩ (dom 𝑥 × ran 𝑥)) ∘ (𝑥 ∩ (dom 𝑥 × ran 𝑥))) S (𝑥 ∩ (dom 𝑥 × ran 𝑥))} |