Definition df-rab 1650

Description: Define a restricted class abstraction (class builder), 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 1646	. 2 class {x ∈ A∣φ}
5	2	cv 954	. . . . 5 class x
6	5, 3	wcel 957	. . . 4 wff x ∈ A
7	6, 1	wa 223	. . 3 wff (x ∈ A ⋀ φ)
8	7, 2	cab 1462	. 2 class {x∣(x ∈ A ⋀ φ)}
9	4, 8	wceq 955	1 wff {x ∈ A∣φ} = {x∣(x ∈ A ⋀ φ)}

This definition is referenced by:  rabid 1767  rabid2 1768  rabswap 1769  hbrab1 1770  hbrab 1771  rabbii 1802  rabbidv 1803  rabeqf 1805  rabab 1819  elrabf 1901  cbvrab 1907  dfin5 2049  dfdif2 2053  ss2rab 2120  rabss 2121  ssrab 2122  rabss2 2126  ssrab2 2128  rabbirdv 2218  unrab 2267  inrab 2268  inrab2 2269  difrab 2270  dfrab2 2271  dfnul3 2280  rabn0 2289  rabsn 2442  elunirab 2510  elintrab 2541  iunrab 2592  intexrab 2728  abssexg 2743  exss 2765  reuuni1 2878  reucl 2881  reusn 2888  orduniss2 3086  dfom2 3129  zfrep6 3610  xp2 4098  unielxp 4100  supex 4560  scottexs 4701  scott0s 4702  kardex 4708  aceq6a 4724  zorn2lem1 4771  zorn2 4779  cardval 4809  cardval2 4838  nnzrab 6114  nn0zrab 6115  iooval2t 6317  sqr0 6617  isumclt 7161  cncnplem1 7734  iscau 7898  issubg 8080  pjmvalt 9193  adjbdlnt 9972  fiv 10433  isfuna 10664

Copyright terms: Public domain