Definition df-rab 1208

Description: Define a restricted class abstraction, which is the class of all x in A such that φ is true. Definition of [TakeutiZaring] p. 20.

Assertion

Ref	Expression
df-rab	⊢ {x ∈ A∣φ} = {x∣(x ∈ A ∧ φ)}

Detailed syntax breakdown of Definition df-rab

Step	Hyp	Ref	Expression
1		wph	. . 3 wff φ
2		vx	. . 3 set x
3		cA	. . 3 class A
4	1, 2, 3	crab 1204	. 2 class {x ∈ A∣φ}
5	2	cv 1089	. . . . 5 class x
6	5, 3	wcel 1092	. . . 4 wff x ∈ A
7	6, 1	wa 196	. . 3 wff (x ∈ A ∧ φ)
8	7, 2	cab 1090	. 2 class {x∣(x ∈ A ∧ φ)}
9	4, 8	wceq 1091	1 wff {x ∈ A∣φ} = {x∣(x ∈ A ∧ φ)}

This definition is referenced by:  rabid 1308  rabid2 1309  hbrab1 1310  hbrab 1311  birabi 1342  birabdv 1343  rabeqf 1345  rabab 1359  elrabf 1421  cbvrab 1425  elabs2 1457  dfdif2 1495  ss2rab 1553  ssrab 1556  birabrdv 1648  unrab 1694  difrab 1695  dfrab2 1696  dfnul3 1710  rabn0 1716  exss 1881  reuuni1 1955  reucl 1957  elintrab 1977  intmin2 1984  intexrab 1988  iunrab 2022  supex 2157  dfom2 2374  zfrep6 2744  scottexs 3543  scott0s 3544  kardex 3550  aceq6a 3564  zornlem1 3603  zorn 3611  cardval 3633  cardval2 3661  nnz 4582  nn0z 4583  sqr0 4730  pjmvalt 5245

metamath.org