Definition df-rab 2425

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 2420	. 2 class { x e. A | ph }
5	2	cv 1330	. . . . 5 class x
6	5, 3	wcel 1480	. . . 4 wff x e. A
7	6, 1	wa 103	. . 3 wff ( x e. A /\ ph )
8	7, 2	cab 2125	. 2 class { x | ( x e. A /\ ph ) }
9	4, 8	wceq 1331	1 wff { x e. A | ph } = { x | ( x e. A /\ ph ) }

This definition is referenced by:  rabid  2606  rabid2  2607  rabbi  2608  rabswap  2609  nfrab1  2610  nfrabxy  2611  rabbiia  2671  rabbidva2  2673  rabeqf  2676  cbvrab  2684  rabab  2707  elrabi  2837  elrabf  2838  elrab3t  2839  ralrab2  2849  rexrab2  2851  cbvrabcsf  3065  dfin5  3078  dfdif2  3079  ss2rab  3173  rabss  3174  ssrab  3175  rabss2  3180  ssrab2  3182  rabssab  3184  notab  3346  unrab  3347  inrab  3348  inrab2  3349  difrab  3350  dfrab2  3351  dfrab3  3352  notrab  3353  rabun2  3355  dfnul3  3366  rabn0r  3389  rabn0m  3390  rab0  3391  rabeq0  3392  dfif6  3476  rabsn  3590  reusn  3594  rabsneu  3596  elunirab  3749  elintrab  3783  ssintrab  3794  iunrab  3860  iinrabm  3875  intexrabim  4078  repizf2  4086  exss  4149  rabxp  4576  exse2  4913  mptpreima  5032  fndmin  5527  fncnvima2  5541  riotauni  5736  riotacl2  5743  snriota  5759  xp2  6071  unielxp  6072  dfopab2  6087  unfiexmid  6806  nnzrab  9078  nn0zrab  9079  shftlem  10588  shftuz  10589  shftdm  10594  negfi  10999  cnblcld  12704  bdcrab  13050