Detailed syntax breakdown of Definition df-se
Step | Hyp | Ref
| Expression |
1 | | cA |
. . 3
class A |
2 | | cR |
. . 3
class 𝑅 |
3 | 1, 2 | wse 4055 |
. 2
wff 𝑅 Se A |
4 | | vy |
. . . . . . 7
setvar y |
5 | 4 | cv 1241 |
. . . . . 6
class y |
6 | | vx |
. . . . . . 7
setvar x |
7 | 6 | cv 1241 |
. . . . . 6
class x |
8 | 5, 7, 2 | wbr 3755 |
. . . . 5
wff y𝑅x |
9 | 8, 4, 1 | crab 2304 |
. . . 4
class {y ∈ A ∣ y𝑅x} |
10 | | cvv 2551 |
. . . 4
class V |
11 | 9, 10 | wcel 1390 |
. . 3
wff {y ∈ A ∣ y𝑅x} ∈
V |
12 | 11, 6, 1 | wral 2300 |
. 2
wff ∀x ∈ A {y ∈ A ∣ y𝑅x} ∈
V |
13 | 3, 12 | wb 98 |
1
wff (𝑅 Se A
↔ ∀x ∈ A {y ∈ A ∣
y𝑅x} ∈ V) |