Definition df-dcin 12990

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 12989	. 2 wff A DECIDin B
4		vx	. . . . . 6 setvar x
5	4	cv 1330	. . . . 5 class x
6	5, 1	wcel 1480	. . . 4 wff x e. A
7	6	wdc 819	. . 3 wff DECID x e. A
8	7, 4, 2	wral 2414	. 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  12991  decidr  12992  sumdc2  12995