Definition df-bj-gab 35122

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

Assertion

Ref	Expression
df-bj-gab	⊢ {𝐴 ∣ 𝑥 ∣ 𝜑} = {𝑦 ∣ ∃𝑥(𝐴 = 𝑦 ∧ 𝜑)}

Distinct variable groups:   𝑥,𝑦   𝑦,𝐴   𝜑,𝑦

Allowed substitution hints:   𝜑(𝑥)   𝐴(𝑥)

Detailed syntax breakdown of Definition df-bj-gab

Step	Hyp	Ref	Expression
1		wph	. . 3 wff 𝜑
2		vx	. . 3 setvar 𝑥
3		cA	. . 3 class 𝐴
4	1, 2, 3	bj-cgab 35121	. 2 class {𝐴 ∣ 𝑥 ∣ 𝜑}
5		vy	. . . . . . 7 setvar 𝑦
6	5	cv 1538	. . . . . 6 class 𝑦
7	3, 6	wceq 1539	. . . . 5 wff 𝐴 = 𝑦
8	7, 1	wa 396	. . . 4 wff (𝐴 = 𝑦 ∧ 𝜑)
9	8, 2	wex 1782	. . 3 wff ∃𝑥(𝐴 = 𝑦 ∧ 𝜑)
10	9, 5	cab 2715	. 2 class {𝑦 ∣ ∃𝑥(𝐴 = 𝑦 ∧ 𝜑)}
11	4, 10	wceq 1539	1 wff {𝐴 ∣ 𝑥 ∣ 𝜑} = {𝑦 ∣ ∃𝑥(𝐴 = 𝑦 ∧ 𝜑)}

This definition is referenced by:  bj-gabss  35123  bj-gabeqis  35126  bj-elgab  35127