Definition df-rab 1652

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

This definition is referenced by:  rabid 1769  rabid2 1770  rabswap 1771  hbrab1 1772  hbrab 1773  rabbii 1805  rabbidv 1806  rabeqf 1808  rabab 1822  elrabf 1904  cbvrab 1910  dfin5 2052  dfdif2 2056  ss2rab 2123  rabss 2124  ssrab 2125  rabss2 2129  ssrab2 2131  rabbirdv 2221  unrab 2270  inrab 2271  inrab2 2272  difrab 2273  dfrab2 2274  dfnul3 2283  rabn0 2292  rabsn 2445  elunirab 2514  elintrab 2545  iunrab 2596  intexrab 2732  abssexg 2747  exss 2769  reuuni1 2882  reucl 2885  reusn 2892  orduniss2 3090  dfom2 3133  zfrep6 3614  xp2 4105  unielxp 4107  supex 4577  scottexs 4718  scott0s 4719  kardex 4725  aceq6a 4741  zorn2lem1 4788  zorn2 4796  cardval 4826  cardval2 4855  nnzrab 6157  nn0zrab 6158  iooval2t 6367  sqr0 6672  isumclt 7209  cncnplem1 7774  iscau 7936  issubg 8116  pjmvalt 9238  adjbdlnt 10016  fiv 10482  fivOLD 10483  isfuna 10754

Copyright terms: Public domain