Definition df-rab 2623

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 2618	. 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  2787  rabid2  2788  rabbi  2789  rabswap  2790  nfrab1  2791  nfrab  2792  rabbiia  2849  rabeqf  2852  cbvrab  2857  rabab  2876  elrabf  2993  ralrab2  3002  rexrab2  3004  cbvrabcsf  3201  dfdif2  3222  ss2rab  3342  rabss  3343  ssrab  3344  rabss2  3349  ssrab2  3351  rabssab  3352  rabbi2dva  3463  notab  3525  unrab  3526  inrab  3527  inrab2  3528  difrab  3529  dfrab2  3530  dfrab3  3531  notrab  3532  rabun2  3534  dfnul3  3553  rabn0  3570  rab0  3571  dfif6  3665  rabsn  3790  reusn  3793  rabsneu  3795  elunirab  3904  elintrab  3938  ssintrab  3949  iunrab  4013  iinrab  4028  reiotacl2  4363  opeq  4619  rabxp  4814  mptpreima  5682  dmmpt  5683  frds  5935  fnpm  6008  pmvalg  6010  mapsspm  6021  dmsnfn  6327