Definition df-rab 1698

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.

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 set x
3		cA	. . 3 class A
4	1, 2, 3	crab 1694	. 2 class {x e. A | ph}
5	2	cv 991	. . . . 5 class x
6	5, 3	wcel 994	. . . 4 wff x e. A
7	6, 1	wa 221	. . 3 wff (x e. A /\ ph)
8	7, 2	cab 1505	. 2 class {x | (x e. A /\ ph)}
9	4, 8	wceq 992	1 wff {x e. A | ph} = {x | (x e. A /\ ph)}

This definition is referenced by:  rabid 1815  rabid2 1816  rabswap 1817  hbrab1 1818  hbrab 1819  rabbii 1851  rabbidv 1852  rabeqf 1854  rabab 1868  elrabf 1950  cbvrab 1956  dfin5 2104  dfdif2 2108  ss2rab 2175  rabss 2176  ssrab 2177  rabss2 2181  ssrab2 2183  rabbirdv 2273  unrab 2322  inrab 2323  inrab2 2324  difrab 2325  dfrab2 2326  dfnul3 2335  rabn0 2345  rabsn 2506  elunirab 2580  reucl 2584  elintrab 2612  iunrab 2664  intexrab 2806  abssexg 2825  exss 2847  reuuni1 3106  reusn 3115  orduniss2 3187  dfom2 3220  zfrep6 3721  xp2 4165  unielxp 4167  supex 4720  scottexs 4864  scott0s 4865  kardex 4871  aceq6a 4887  zorn2lem1 4934  zorn2 4942  cardval 4973  cardval2 5005  nnzrab 6325  nn0zrab 6326  iooval2 6493  sqr0 6873  isumcl 7413  cncnplem1 7984  iscau 8147  issubg 8358  pjmval 9514  adjbdln 10295  fiv 10849  zrdivrng 10969  isfuna 11288  ordtypelem1 11427  ordtypelem6 11432  ordtype 11434  neibastop2lem3 11582  neibastop2lem4 11583  topjoin 11588  ist1-3 11604  filufint 11659  fixufil 11661  totbndbnd 12000

Copyright terms: Public domain