MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-opab Unicode version

Definition df-opab 4377
Description: Define the class abstraction of a collection of ordered pairs. Definition 3.3 of [Monk1] p. 34. Usually and are distinct, although the definition doesn't strictly require it (see dfid2 4659 for a case where they are not distinct). The brace notation is called "class abstraction" by Quine; it is also (more commonly) called a "class builder" in the literature. An alternate definition using no existential quantifiers is shown by dfopab2 6634. For example, ={<. , >.|( e. /\ e. /\( 1)= )}->3 4 (ex-opab 22761). (Contributed by NM, 4-Jul-1994.)
Assertion
Ref Expression
df-opab
Distinct variable groups:   ,   ,   ,
Allowed substitution hints:   ( , )

Detailed syntax breakdown of Definition df-opab
StepHypRef Expression
1 wph . . 3
2 vx . . 3
3 vy . . 3
41, 2, 3copab 4375 . 2
5 vz . . . . . . . 8
65cv 1669 . . . . . . 7
72cv 1669 . . . . . . . 8
83cv 1669 . . . . . . . 8
97, 8cop 3912 . . . . . . 7
106, 9wceq 1670 . . . . . 6
1110, 1wa 360 . . . . 5
1211, 3wex 1565 . . . 4
1312, 2wex 1565 . . 3
1413, 5cab 2475 . 2
154, 14wceq 1670 1
Colors of variables: wff set class
This definition is referenced by:  opabss  4379  opabbid  4380  nfopab  4383  nfopab1  4384  nfopab2  4385  cbvopab  4386  cbvopab1  4388  cbvopab2  4389  cbvopab1s  4390  cbvopab2v  4392  unopab  4393  opabid  4618  elopab  4619  ssopab2  4637  iunopab  4645  dfid3  4658  elxpi  4878  rabxp  4897  csbxp  4940  csbxpgOLD  4941  relopabi  4987  opabbrex  6142  dfoprab2  6145  dmoprab  6183  dfopab2  6634  brdom7disj  8580  brdom6disj  8581  swrd0  12174  cnvoprab  25153  areacirc  27669  dropab1  28877  dropab2  28878  csbxpgVD  30476  relopabVD  30483
  Copyright terms: Public domain W3C validator