Definition df-cc 7330

Description: The expression CCHOICE will be used as a readable shorthand for any form of countable choice, analogous to df-ac 7273 for full choice. (Contributed by Jim Kingdon, 27-Nov-2023.)

Assertion

Ref	Expression
df-cc	|- (CCHOICE <-> A. x ( dom x ~~ om -> E. f ( f C_ x /\ f Fn dom x ) ) )

Distinct variable group:   x, f

Detailed syntax breakdown of Definition df-cc

Step	Hyp	Ref	Expression
1		wacc 7329	. 2 wff CCHOICE
2		vx	. . . . . . 7 setvar x
3	2	cv 1363	. . . . . 6 class x
4	3	cdm 4663	. . . . 5 class dom x
5		com 4626	. . . . 5 class om
6		cen 6797	. . . . 5 class ~~
7	4, 5, 6	wbr 4033	. . . 4 wff dom x ~~ om
8		vf	. . . . . . . 8 setvar f
9	8	cv 1363	. . . . . . 7 class f
10	9, 3	wss 3157	. . . . . 6 wff f C_ x
11	9, 4	wfn 5253	. . . . . 6 wff f Fn dom x
12	10, 11	wa 104	. . . . 5 wff ( f C_ x /\ f Fn dom x )
13	12, 8	wex 1506	. . . 4 wff E. f ( f C_ x /\ f Fn dom x )
14	7, 13	wi 4	. . 3 wff ( dom x ~~ om -> E. f ( f C_ x /\ f Fn dom x ) )
15	14, 2	wal 1362	. 2 wff A. x ( dom x ~~ om -> E. f ( f C_ x /\ f Fn dom x ) )
16	1, 15	wb 105	1 wff (CCHOICE <-> A. x ( dom x ~~ om -> E. f ( f C_ x /\ f Fn dom x ) ) )

This definition is referenced by:  ccfunen  7331