Definition df-dcin 15440

Description: Define decidability of a class in another. (Contributed by BJ, 19-Feb-2022.)

Assertion

Ref	Expression
df-dcin	|- ( A DECIDin B <-> A. x e. B DECID x e. A )

Distinct variable groups:   x, A   x, B

Detailed syntax breakdown of Definition df-dcin

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2		cB	. . 3 class B
3	1, 2	wdcin 15439	. 2 wff A DECIDin B
4		vx	. . . . . 6 setvar x
5	4	cv 1363	. . . . 5 class x
6	5, 1	wcel 2167	. . . 4 wff x e. A
7	6	wdc 835	. . 3 wff DECID x e. A
8	7, 4, 2	wral 2475	. 2 wff A. x e. B DECID x e. A
9	3, 8	wb 105	1 wff ( A DECIDin B <-> A. x e. B DECID x e. A )

This definition is referenced by:  decidi  15441  decidr  15442  sumdc2  15445