Definition df-dcin 13829

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 13828	. 2 wff A DECIDin B
4		vx	. . . . . 6 setvar x
5	4	cv 1347	. . . . 5 class x
6	5, 1	wcel 2141	. . . 4 wff x e. A
7	6	wdc 829	. . 3 wff DECID x e. A
8	7, 4, 2	wral 2448	. 2 wff A. x e. B DECID x e. A
9	3, 8	wb 104	1 wff ( A DECIDin B <-> A. x e. B DECID x e. A )

This definition is referenced by:  decidi  13830  decidr  13831  sumdc2  13834