HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Definition df-rab 1644
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
StepHypRef Expression
1 wph . . 3 wff ph
2 vx . . 3 set x
3 cA . . 3 class A
41, 2, 3crab 1640 . 2 class {x e. A | ph}
52cv 952 . . . . 5 class x
65, 3wcel 955 . . . 4 wff x e. A
76, 1wa 223 . . 3 wff (x e. A /\ ph)
87, 2cab 1456 . 2 class {x | (x e. A /\ ph)}
94, 8wceq 953 1 wff {x e. A | ph} = {x | (x e. A /\ ph)}
Colors of variables: wff set class
This definition is referenced by:  rabid 1761  rabid2 1762  rabswap 1763  hbrab1 1764  hbrab 1765  rabbii 1796  rabbidv 1797  rabeqf 1799  rabab 1813  elrabf 1895  cbvrab 1901  dfin5 2042  dfdif2 2046  ss2rab 2113  rabss 2114  ssrab 2115  rabss2 2119  ssrab2 2121  rabbirdv 2211  unrab 2260  inrab 2261  inrab2 2262  difrab 2263  dfrab2 2264  dfnul3 2273  rabn0 2282  rabsn 2435  elunirab 2504  elintrab 2535  iunrab 2586  intexrab 2722  abssexg 2737  exss 2759  reuuni1 2872  reucl 2875  reusn 2882  orduniss2 3080  dfom2 3123  zfrep6 3600  xp2 4089  unielxp 4091  supex 4551  scottexs 4690  scott0s 4691  kardex 4697  aceq6a 4713  zorn2lem1 4760  zorn2 4768  cardval 4798  cardval2 4827  nnzrab 6104  nn0zrab 6105  iooval2t 6304  sqr0 6602  isumclt 7144  cncnplem1 7713  iscau 7874  issubg 8053  pjmvalt 9153  adjbdlnt 9931  fiv 10374  isfuna 10592
Copyright terms: Public domain