Definition df-rab 2289

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 2284	. 2 class {x ∈ A ∣ φ}
5	2	cv 1225	. . . . 5 class x
6	5, 3	wcel 1370	. . . 4 wff x ∈ A
7	6, 1	wa 97	. . 3 wff (x ∈ A ∧ φ)
8	7, 2	cab 2004	. 2 class {x ∣ (x ∈ A ∧ φ)}
9	4, 8	wceq 1226	1 wff {x ∈ A ∣ φ} = {x ∣ (x ∈ A ∧ φ)}

This definition is referenced by:  rabid  2459  rabid2  2460  rabbi  2461  rabswap  2462  nfrab1  2463  nfrabxy  2464  rabbiia  2521  rabeqf  2524  cbvrab  2529  rabab  2548  elrabi  2668  elrabf  2669  elrab3t  2670  ralrab2  2679  rexrab2  2681  cbvrabcsf  2884  dfin5  2898  dfdif2  2899  ss2rab  2989  rabss  2990  ssrab  2991  rabss2  2996  ssrab2  2998  rabssab  3000  notab  3180  unrab  3181  inrab  3182  inrab2  3183  difrab  3184  dfrab2  3185  dfrab3  3186  notrab  3187  rabun2  3189  dfnul3  3200  rabn0r  3217  rabn0m  3218  rab0  3219  rabeq0  3220  dfif6  3308  rabsn  3407  reusn  3411  rabsneu  3413  elunirab  3563  elintrab  3597  ssintrab  3608  iunrab  3674  iinrabm  3689  intexrabim  3877  repizf2  3885  exss  3933  rabxp  4303  exse2  4622  mptpreima  4737  fndmin  5195  fncnvima2  5209  riotauni  5394  riotacl2  5401  snriota  5417  xp2  5718  unielxp  5719  dfopab2  5734  bdcrab  7218