Detailed syntax breakdown of Definition df-prt
Step | Hyp | Ref
| Expression |
1 | | cA |
. . 3
class 𝐴 |
2 | 1 | wprt 36649 |
. 2
wff Prt 𝐴 |
3 | | vx |
. . . . . 6
setvar 𝑥 |
4 | | vy |
. . . . . 6
setvar 𝑦 |
5 | 3, 4 | weq 1971 |
. . . . 5
wff 𝑥 = 𝑦 |
6 | 3 | cv 1542 |
. . . . . . 7
class 𝑥 |
7 | 4 | cv 1542 |
. . . . . . 7
class 𝑦 |
8 | 6, 7 | cin 3880 |
. . . . . 6
class (𝑥 ∩ 𝑦) |
9 | | c0 4252 |
. . . . . 6
class
∅ |
10 | 8, 9 | wceq 1543 |
. . . . 5
wff (𝑥 ∩ 𝑦) = ∅ |
11 | 5, 10 | wo 847 |
. . . 4
wff (𝑥 = 𝑦 ∨ (𝑥 ∩ 𝑦) = ∅) |
12 | 11, 4, 1 | wral 3062 |
. . 3
wff
∀𝑦 ∈
𝐴 (𝑥 = 𝑦 ∨ (𝑥 ∩ 𝑦) = ∅) |
13 | 12, 3, 1 | wral 3062 |
. 2
wff
∀𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐴 (𝑥 = 𝑦 ∨ (𝑥 ∩ 𝑦) = ∅) |
14 | 2, 13 | wb 209 |
1
wff (Prt 𝐴 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 = 𝑦 ∨ (𝑥 ∩ 𝑦) = ∅)) |