Definition df-rab 1649

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 1645	. 2 class {x e. A | ph}
5	2	cv 953	. . . . 5 class x
6	5, 3	wcel 956	. . . 4 wff x e. A
7	6, 1	wa 223	. . 3 wff (x e. A /\ ph)
8	7, 2	cab 1461	. 2 class {x | (x e. A /\ ph)}
9	4, 8	wceq 954	1 wff {x e. A | ph} = {x | (x e. A /\ ph)}

This definition is referenced by:  rabid 1766  rabid2 1767  rabswap 1768  hbrab1 1769  hbrab 1770  rabbii 1801  rabbidv 1802  rabeqf 1804  rabab 1818  elrabf 1900  cbvrab 1906  dfin5 2048  dfdif2 2052  ss2rab 2119  rabss 2120  ssrab 2121  rabss2 2125  ssrab2 2127  rabbirdv 2217  unrab 2266  inrab 2267  inrab2 2268  difrab 2269  dfrab2 2270  dfnul3 2279  rabn0 2288  rabsn 2441  elunirab 2509  elintrab 2540  iunrab 2591  intexrab 2727  abssexg 2742  exss 2764  reuuni1 2877  reucl 2880  reusn 2887  orduniss2 3085  dfom2 3128  zfrep6 3606  xp2 4095  unielxp 4097  supex 4557  scottexs 4698  scott0s 4699  kardex 4705  aceq6a 4721  zorn2lem1 4768  zorn2 4776  cardval 4806  cardval2 4835  nnzrab 6112  nn0zrab 6113  iooval2t 6312  sqr0 6610  isumclt 7152  cncnplem1 7724  iscau 7888  issubg 8068  pjmvalt 9176  adjbdlnt 9954  fiv 10410  isfuna 10628

Copyright terms: Public domain