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

Definition df-opab 4302
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 4541 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 6451. For example, ?Error: CC /\ y e. CC /\ ( x + 1 ) = y ) } -> 3 R 4 ^^ This math symbol is not active (i.e. was not declared in this scope). ={<. , >.|( e. /\ e. /\( 1)= )}->3 4 (ex-opab 21791). (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 4300 . 2
5 vz . . . . . . . 8
65cv 1653 . . . . . . 7
72cv 1653 . . . . . . . 8
83cv 1653 . . . . . . . 8
97, 8cop 3844 . . . . . . 7
106, 9wceq 1654 . . . . . 6
1110, 1wa 360 . . . . 5
1211, 3wex 1551 . . . 4
1312, 2wex 1551 . . 3
1413, 5cab 2429 . 2
154, 14wceq 1654 1
Colors of variables: wff set class
This definition is referenced by:  opabss  4304  opabbid  4305  nfopab  4308  nfopab1  4309  nfopab2  4310  cbvopab  4311  cbvopab1  4313  cbvopab2  4314  cbvopab1s  4315  cbvopab2v  4317  unopab  4318  opabid  4500  elopab  4501  ssopab2  4519  iunopab  4527  dfid3  4540  elxpi  4935  rabxp  4954  csbxp  4997  csbxpgOLD  4998  relopabi  5042  opabbrex  6168  dfoprab2  6171  dmoprab  6204  dfopab2  6451  brdom7disj  8460  brdom6disj  8461  cnvoprab  24717  areacirc  26408  dropab1  27805  dropab2  27806  csbxpgVD  29247  relopabVD  29254
  Copyright terms: Public domain W3C validator