Definition df-rab 2624

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 2619	. 2 class {x ∈ A ∣ φ}
5	2	cv 1641	. . . . 5 class x
6	5, 3	wcel 1710	. . . 4 wff x ∈ A
7	6, 1	wa 358	. . 3 wff (x ∈ A ∧ φ)
8	7, 2	cab 2339	. 2 class {x ∣ (x ∈ A ∧ φ)}
9	4, 8	wceq 1642	1 wff {x ∈ A ∣ φ} = {x ∣ (x ∈ A ∧ φ)}

This definition is referenced by:  rabid  2788  rabid2  2789  rabbi  2790  rabswap  2791  nfrab1  2792  nfrab  2793  rabbiia  2850  rabeqf  2853  cbvrab  2858  rabab  2877  elrabf  2994  ralrab2  3003  rexrab2  3005  cbvrabcsf  3202  dfdif2  3223  ss2rab  3343  rabss  3344  ssrab  3345  rabss2  3350  ssrab2  3352  rabssab  3353  rabbi2dva  3464  notab  3526  unrab  3527  inrab  3528  inrab2  3529  difrab  3530  dfrab2  3531  dfrab3  3532  notrab  3533  rabun2  3535  dfnul3  3554  rabn0  3571  rab0  3572  dfif6  3666  rabsn  3791  reusn  3794  rabsneu  3796  elunirab  3905  elintrab  3939  ssintrab  3950  iunrab  4014  iinrab  4029  reiotacl2  4364  opeq  4620  rabxp  4815  mptpreima  5683  dmmpt  5684  frds  5936  fnpm  6009  pmvalg  6011  mapsspm  6022  dmsnfn  6328