Definition df-bj-gab

Description: Definition of generalized class abstractions: typically, x is a bound variable in A and ph and { A | x | ph } denotes "the class of A ( x ) 's such that ph ( x ) ". (Contributed by BJ, 4-Oct-2024)

	Ref	Expression
Assertion	df-bj-gab	Could not format assertion : No typesetting found for |- {{ A | x | ph }} = { y | E. x ( A = y /\ ph ) } with typecode |-

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	$$classA$$
1		vx	$$setvarx$$
2		wph	$$wff\phi$$
3	2 1 0	bj-cgab	Could not format {{ A | x | ph }} : No typesetting found for class {{ A | x | ph }} with typecode class
4		vy	$$setvary$$
5	4	cv	$$setvary$$
6	0 5	wceq	$$wffA=y$$
7	6 2	wa	$$wff\left(A=y\wedge \phi \right)$$
8	7 1	wex	$$wff\exists x\left(A=y\wedge \phi \right)$$
9	8 4	cab	$$class\left\{y|\exists x\left(A=y\wedge \phi \right)\right\}$$
10	3 9	wceq	Could not format {{ A | x | ph }} = { y | E. x ( A = y /\ ph ) } : No typesetting found for wff {{ A | x | ph }} = { y | E. x ( A = y /\ ph ) } with typecode wff