Definition df-rab 2529

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

Assertion

Ref	Expression
df-rab	|- { x e. A | ph } = { x | ( x e. A /\ ph ) }

Detailed syntax breakdown of Definition df-rab

Step	Hyp	Ref	Expression
1		wph	. . 3 wff ph
2		vx	. . 3 setvar x
3		cA	. . 3 class A
4	1, 2, 3	crab 2524	. 2 class { x e. A | ph }
5	2	cv 1397	. . . . 5 class x
6	5, 3	wcel 2203	. . . 4 wff x e. A
7	6, 1	wa 104	. . 3 wff ( x e. A /\ ph )
8	7, 2	cab 2218	. 2 class { x | ( x e. A /\ ph ) }
9	4, 8	wceq 1398	1 wff { x e. A | ph } = { x | ( x e. A /\ ph ) }

This definition is referenced by:  rabid  2719  rabid2  2720  rabbi  2721  rabswap  2722  nfrab1  2723  nfrabw  2724  rabbidva2  2796  rabbiia  2798  rabeqf  2802  cbvrab  2810  rabab  2834  elrabi  2969  elrabf  2970  elrab3t  2971  ralrab2  2981  rexrab2  2983  cbvrabcsf  3203  dfin5  3217  dfdif2  3218  ss2rab  3313  rabss  3314  ssrab  3315  rabss2  3320  ssrab2  3322  rabssab  3326  notab  3490  unrab  3491  inrab  3492  inrab2  3493  difrab  3494  dfrab2  3495  dfrab3  3496  notrab  3497  rabun2  3499  dfnul3  3510  rabn0r  3534  rabn0m  3535  rab0  3536  rabeq0  3537  dfif6  3621  rabsn  3755  rabsnifsb  3756  reusn  3761  rabsneu  3763  elunirab  3926  elintrab  3960  ssintrab  3971  iunrab  4038  iinrabm  4053  intexrabim  4264  repizf2  4274  exss  4342  rabxp  4786  exse2  5135  mptpreima  5255  fndmin  5784  fncnvima2  5798  riotauni  6009  riotacl2  6017  snriota  6034  xp2  6366  unielxp  6367  dfopab2  6382  ressuppss  6453  unfiexmid  7177  nnzrab  9600  nn0zrab  9601  wrdnval  11251  shftlem  11497  shftuz  11498  shftdm  11503  negfi  11909  eqglact  13934  dfrhm2  14291  cnblcld  15392  2lgslem1b  15954  vtxdfifiun  16284  bdcrab  16614