Definition df-rab 2309

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

Assertion

Ref	Expression
df-rab	⊢ {x ∈ A ∣ φ} = {x ∣ (x ∈ A ∧ φ)}

Detailed syntax breakdown of Definition df-rab

Step	Hyp	Ref	Expression
1		wph	. . 3 wff φ
2		vx	. . 3 setvar x
3		cA	. . 3 class A
4	1, 2, 3	crab 2304	. 2 class {x ∈ A ∣ φ}
5	2	cv 1241	. . . . 5 class x
6	5, 3	wcel 1390	. . . 4 wff x ∈ A
7	6, 1	wa 97	. . 3 wff (x ∈ A ∧ φ)
8	7, 2	cab 2023	. 2 class {x ∣ (x ∈ A ∧ φ)}
9	4, 8	wceq 1242	1 wff {x ∈ A ∣ φ} = {x ∣ (x ∈ A ∧ φ)}

This definition is referenced by:  rabid  2479  rabid2  2480  rabbi  2481  rabswap  2482  nfrab1  2483  nfrabxy  2484  rabbiia  2541  rabeqf  2544  cbvrab  2549  rabab  2569  elrabi  2689  elrabf  2690  elrab3t  2691  ralrab2  2700  rexrab2  2702  cbvrabcsf  2905  dfin5  2919  dfdif2  2920  ss2rab  3010  rabss  3011  ssrab  3012  rabss2  3017  ssrab2  3019  rabssab  3021  notab  3201  unrab  3202  inrab  3203  inrab2  3204  difrab  3205  dfrab2  3206  dfrab3  3207  notrab  3208  rabun2  3210  dfnul3  3221  rabn0r  3238  rabn0m  3239  rab0  3240  rabeq0  3241  dfif6  3327  rabsn  3428  reusn  3432  rabsneu  3434  elunirab  3584  elintrab  3618  ssintrab  3629  iunrab  3695  iinrabm  3710  intexrabim  3898  repizf2  3906  exss  3954  rabxp  4323  exse2  4642  mptpreima  4757  fndmin  5217  fncnvima2  5231  riotauni  5417  riotacl2  5424  snriota  5440  xp2  5741  unielxp  5742  dfopab2  5757  nnzrab  8045  nn0zrab  8046  bdcrab  9307