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

Definition df-opab 5121
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 does not require it (see dfid2 5457 for a case where they are not distinct). The brace notation is called "class abstraction" by Quine; it is also called "class builder" in the literature. An alternate definition using no existential quantifiers is shown by dfopab2 7741. An example is given by ex-opab 28139. (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 wff 𝜑
2 vx . . 3 setvar 𝑥
3 vy . . 3 setvar 𝑦
41, 2, 3copab 5120 . 2 class {⟨𝑥, 𝑦⟩ ∣ 𝜑}
5 vz . . . . . . . 8 setvar 𝑧
65cv 1527 . . . . . . 7 class 𝑧
72cv 1527 . . . . . . . 8 class 𝑥
83cv 1527 . . . . . . . 8 class 𝑦
97, 8cop 4565 . . . . . . 7 class 𝑥, 𝑦
106, 9wceq 1528 . . . . . 6 wff 𝑧 = ⟨𝑥, 𝑦
1110, 1wa 396 . . . . 5 wff (𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)
1211, 3wex 1771 . . . 4 wff 𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)
1312, 2wex 1771 . . 3 wff 𝑥𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)
1413, 5cab 2799 . 2 class {𝑧 ∣ ∃𝑥𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)}
154, 14wceq 1528 1 wff {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {𝑧 ∣ ∃𝑥𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)}
Colors of variables: wff setvar class
This definition is referenced by:  opabss  5122  opabbid  5123  nfopab  5126  nfopab1  5127  nfopab2  5128  cbvopab  5129  cbvopab1  5131  cbvopab1g  5132  cbvopab2  5133  cbvopab1s  5134  cbvopab2v  5136  unopab  5137  opabidw  5404  opabid  5405  elopab  5406  ssopab2  5425  iunopab  5438  dfid3  5456  elxpi  5571  rabxp  5594  csbxp  5644  ssrel  5651  relopabi  5688  relopabiALT  5689  opabssxpd  5783  cnv0  5993  dfoprab2  7201  dmoprab  7244  dfopab2  7741  brdom7disj  9942  brdom6disj  9943  opabssi  30293  cnvoprabOLD  30383  rnxrn  35528  dropab1  40659  dropab2  40660  csbxpgVD  41108  relopabVD  41115
  Copyright terms: Public domain W3C validator