Definition df-rab 2464

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 2459	. 2 class { x e. A | ph }
5	2	cv 1352	. . . . 5 class x
6	5, 3	wcel 2148	. . . 4 wff x e. A
7	6, 1	wa 104	. . 3 wff ( x e. A /\ ph )
8	7, 2	cab 2163	. 2 class { x | ( x e. A /\ ph ) }
9	4, 8	wceq 1353	1 wff { x e. A | ph } = { x | ( x e. A /\ ph ) }

This definition is referenced by:  rabid  2653  rabid2  2654  rabbi  2655  rabswap  2656  nfrab1  2657  nfrabxy  2658  rabbiia  2724  rabbidva2  2726  rabeqf  2729  cbvrab  2737  rabab  2760  elrabi  2892  elrabf  2893  elrab3t  2894  ralrab2  2904  rexrab2  2906  cbvrabcsf  3124  dfin5  3138  dfdif2  3139  ss2rab  3233  rabss  3234  ssrab  3235  rabss2  3240  ssrab2  3242  rabssab  3245  notab  3407  unrab  3408  inrab  3409  inrab2  3410  difrab  3411  dfrab2  3412  dfrab3  3413  notrab  3414  rabun2  3416  dfnul3  3427  rabn0r  3451  rabn0m  3452  rab0  3453  rabeq0  3454  dfif6  3538  rabsn  3661  reusn  3665  rabsneu  3667  elunirab  3824  elintrab  3858  ssintrab  3869  iunrab  3936  iinrabm  3951  intexrabim  4155  repizf2  4164  exss  4229  rabxp  4665  exse2  5004  mptpreima  5124  fndmin  5625  fncnvima2  5639  riotauni  5839  riotacl2  5846  snriota  5862  xp2  6176  unielxp  6177  dfopab2  6192  unfiexmid  6919  nnzrab  9279  nn0zrab  9280  shftlem  10827  shftuz  10828  shftdm  10833  negfi  11238  eqglact  13089  cnblcld  14074  if0ab  14596  bdcrab  14643