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	⊢ { 𝐴 ∣ 𝑥 ∣ 𝜑 } = { 𝑦 ∣ ∃ 𝑥 ( 𝐴 = 𝑦 ∧ 𝜑 ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	⊢ 𝐴
1		vx	⊢ 𝑥
2		wph	⊢ 𝜑
3	2 1 0	bj-cgab	⊢ { 𝐴 ∣ 𝑥 ∣ 𝜑 }
4		vy	⊢ 𝑦
5	4	cv	⊢ 𝑦
6	0 5	wceq	⊢ 𝐴 = 𝑦
7	6 2	wa	⊢ ( 𝐴 = 𝑦 ∧ 𝜑 )
8	7 1	wex	⊢ ∃ 𝑥 ( 𝐴 = 𝑦 ∧ 𝜑 )
9	8 4	cab	⊢ { 𝑦 ∣ ∃ 𝑥 ( 𝐴 = 𝑦 ∧ 𝜑 ) }
10	3 9	wceq	⊢ { 𝐴 ∣ 𝑥 ∣ 𝜑 } = { 𝑦 ∣ ∃ 𝑥 ( 𝐴 = 𝑦 ∧ 𝜑 ) }