Definition df-rab 1628

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 1624	. 2 class {x e. A | ph}
5	2	cv 1098	. . . . 5 class x
6	5, 3	wcel 1105	. . . 4 wff x e. A
7	6, 1	wa 223	. . 3 wff (x e. A /\ ph)
8	7, 2	cab 1440	. 2 class {x | (x e. A /\ ph)}
9	4, 8	wceq 1099	1 wff {x e. A | ph} = {x | (x e. A /\ ph)}

This definition is referenced by:  rabid 1745  rabid2 1746  rabswap 1747  hbrab1 1748  hbrab 1749  rabbii 1780  rabbidv 1781  rabeqf 1783  rabab 1797  elrabf 1876  cbvrab 1882  dfin5 2023  dfdif2 2027  ss2rab 2094  rabss 2095  ssrab 2096  rabss2 2100  ssrab2 2102  rabbirdv 2192  unrab 2241  inrab 2242  inrab2 2243  difrab 2244  dfrab2 2245  dfnul3 2254  rabn0 2263  rabsn 2415  elunirab 2482  elintrab 2513  iunrab 2564  intexrab 2700  abssexg 2715  exss 2737  reuuni1 2845  reucl 2848  reusn 2855  orduniss2 3053  dfom2 3096  zfrep6 3554  xp2 4043  unielxp 4045  supex 4503  scottexs 4642  scott0s 4643  kardex 4649  aceq6a 4665  zorn2lem1 4712  zorn2 4720  cardval 4750  cardval2 4778  nnzrab 6055  nn0zrab 6056  iooval2t 6255  sqr0 6553  isumclt 7095  cncnplem1 7661  iscau 7822  issubg 8001  fiv 8731  isfuna 8940  pjmvalt 9367  adjbdlnt 10145

Copyright terms: Public domain