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 4638
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 4945 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 7090. For example, 𝑅 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ (𝑥 + 1) = 𝑦)} → 3𝑅4 (ex-opab 26474). (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 4636 . 2 class {⟨𝑥, 𝑦⟩ ∣ 𝜑}
5 vz . . . . . . . 8 setvar 𝑧
65cv 1473 . . . . . . 7 class 𝑧
72cv 1473 . . . . . . . 8 class 𝑥
83cv 1473 . . . . . . . 8 class 𝑦
97, 8cop 4130 . . . . . . 7 class 𝑥, 𝑦
106, 9wceq 1474 . . . . . 6 wff 𝑧 = ⟨𝑥, 𝑦
1110, 1wa 382 . . . . 5 wff (𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)
1211, 3wex 1694 . . . 4 wff 𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)
1312, 2wex 1694 . . 3 wff 𝑥𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)
1413, 5cab 2595 . 2 class {𝑧 ∣ ∃𝑥𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)}
154, 14wceq 1474 1 wff {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {𝑧 ∣ ∃𝑥𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)}
Colors of variables: wff setvar class
This definition is referenced by:  opabss  4640  opabbid  4641  nfopab  4644  nfopab1  4645  nfopab2  4646  cbvopab  4647  cbvopab1  4649  cbvopab2  4650  cbvopab1s  4651  cbvopab2v  4653  unopab  4654  opabid  4896  elopab  4897  ssopab2  4915  iunopab  4925  dfid3  4943  elxpi  5043  rabxp  5067  csbxp  5112  relopabi  5155  dfoprab2  6576  dmoprab  6616  opabex2  6974  dfopab2  7090  brdom7disj  9211  brdom6disj  9212  cnvoprab  28679  dropab1  37455  dropab2  37456  csbxpgOLD  37858  csbxpgVD  37935  relopabVD  37942
  Copyright terms: Public domain W3C validator