Metamath Proof Explorer


Definition df-ufl

Description: Define the class of base sets for which the ultrafilter lemma filssufil holds. (Contributed by Mario Carneiro, 26-Aug-2015)

Ref Expression
Assertion df-ufl UFL = x | f Fil x g UFil x f g

Detailed syntax breakdown

Step Hyp Ref Expression
0 cufl class UFL
1 vx setvar x
2 vf setvar f
3 cfil class Fil
4 1 cv setvar x
5 4 3 cfv class Fil x
6 vg setvar g
7 cufil class UFil
8 4 7 cfv class UFil x
9 2 cv setvar f
10 6 cv setvar g
11 9 10 wss wff f g
12 11 6 8 wrex wff g UFil x f g
13 12 2 5 wral wff f Fil x g UFil x f g
14 13 1 cab class x | f Fil x g UFil x f g
15 0 14 wceq wff UFL = x | f Fil x g UFil x f g