Definition df-rab 2451

Description: Define a restricted class abstraction (class builder), which is the class of all 𝑥 in 𝐴 such that 𝜑 is true. Definition of [TakeutiZaring] p. 20. (Contributed by NM, 22-Nov-1994.)

Assertion

Ref	Expression
df-rab	⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}

Detailed syntax breakdown of Definition df-rab

Step	Hyp	Ref	Expression
1		wph	. . 3 wff 𝜑
2		vx	. . 3 setvar 𝑥
3		cA	. . 3 class 𝐴
4	1, 2, 3	crab 2446	. 2 class {𝑥 ∈ 𝐴 ∣ 𝜑}
5	2	cv 1341	. . . . 5 class 𝑥
6	5, 3	wcel 2135	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wa 103	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝜑)
8	7, 2	cab 2150	. 2 class {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}
9	4, 8	wceq 1342	1 wff {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}

This definition is referenced by:  rabid  2639  rabid2  2640  rabbi  2641  rabswap  2642  nfrab1  2643  nfrabxy  2644  rabbiia  2706  rabbidva2  2708  rabeqf  2711  cbvrab  2719  rabab  2742  elrabi  2874  elrabf  2875  elrab3t  2876  ralrab2  2886  rexrab2  2888  cbvrabcsf  3105  dfin5  3118  dfdif2  3119  ss2rab  3213  rabss  3214  ssrab  3215  rabss2  3220  ssrab2  3222  rabssab  3225  notab  3387  unrab  3388  inrab  3389  inrab2  3390  difrab  3391  dfrab2  3392  dfrab3  3393  notrab  3394  rabun2  3396  dfnul3  3407  rabn0r  3430  rabn0m  3431  rab0  3432  rabeq0  3433  dfif6  3517  rabsn  3637  reusn  3641  rabsneu  3643  elunirab  3796  elintrab  3830  ssintrab  3841  iunrab  3907  iinrabm  3922  intexrabim  4126  repizf2  4135  exss  4199  rabxp  4635  exse2  4972  mptpreima  5091  fndmin  5586  fncnvima2  5600  riotauni  5798  riotacl2  5805  snriota  5821  xp2  6133  unielxp  6134  dfopab2  6149  unfiexmid  6874  nnzrab  9206  nn0zrab  9207  shftlem  10744  shftuz  10745  shftdm  10750  negfi  11155  cnblcld  13076  if0ab  13522  bdcrab  13569