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	|- {{ A | x | ph }} = { y | E. x ( A = y /\ ph ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	|- A
1		vx	|- x
2		wph	|- ph
3	2 1 0	bj-cgab	|- {{ A | x | ph }}
4		vy	|- y
5	4	cv	|- y
6	0 5	wceq	|- A = y
7	6 2	wa	|- ( A = y /\ ph )
8	7 1	wex	|- E. x ( A = y /\ ph )
9	8 4	cab	|- { y | E. x ( A = y /\ ph ) }
10	3 9	wceq	|- {{ A | x | ph }} = { y | E. x ( A = y /\ ph ) }