Detailed syntax breakdown of Definition df-ufl
Step | Hyp | Ref
| Expression |
1 | | cufl 21704 |
. 2
class
UFL |
2 | | vf |
. . . . . . 7
setvar 𝑓 |
3 | 2 | cv 1482 |
. . . . . 6
class 𝑓 |
4 | | vg |
. . . . . . 7
setvar 𝑔 |
5 | 4 | cv 1482 |
. . . . . 6
class 𝑔 |
6 | 3, 5 | wss 3574 |
. . . . 5
wff 𝑓 ⊆ 𝑔 |
7 | | vx |
. . . . . . 7
setvar 𝑥 |
8 | 7 | cv 1482 |
. . . . . 6
class 𝑥 |
9 | | cufil 21703 |
. . . . . 6
class
UFil |
10 | 8, 9 | cfv 5888 |
. . . . 5
class
(UFil‘𝑥) |
11 | 6, 4, 10 | wrex 2913 |
. . . 4
wff
∃𝑔 ∈
(UFil‘𝑥)𝑓 ⊆ 𝑔 |
12 | | cfil 21649 |
. . . . 5
class
Fil |
13 | 8, 12 | cfv 5888 |
. . . 4
class
(Fil‘𝑥) |
14 | 11, 2, 13 | wral 2912 |
. . 3
wff
∀𝑓 ∈
(Fil‘𝑥)∃𝑔 ∈ (UFil‘𝑥)𝑓 ⊆ 𝑔 |
15 | 14, 7 | cab 2608 |
. 2
class {𝑥 ∣ ∀𝑓 ∈ (Fil‘𝑥)∃𝑔 ∈ (UFil‘𝑥)𝑓 ⊆ 𝑔} |
16 | 1, 15 | wceq 1483 |
1
wff UFL =
{𝑥 ∣ ∀𝑓 ∈ (Fil‘𝑥)∃𝑔 ∈ (UFil‘𝑥)𝑓 ⊆ 𝑔} |