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 4857
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 5169 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 7381. For example, 𝑅 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ (𝑥 + 1) = 𝑦)} → 3𝑅4 (ex-opab 27592). (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 4856 . 2 class {⟨𝑥, 𝑦⟩ ∣ 𝜑}
5 vz . . . . . . . 8 setvar 𝑧
65cv 1623 . . . . . . 7 class 𝑧
72cv 1623 . . . . . . . 8 class 𝑥
83cv 1623 . . . . . . . 8 class 𝑦
97, 8cop 4319 . . . . . . 7 class 𝑥, 𝑦
106, 9wceq 1624 . . . . . 6 wff 𝑧 = ⟨𝑥, 𝑦
1110, 1wa 383 . . . . 5 wff (𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)
1211, 3wex 1845 . . . 4 wff 𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)
1312, 2wex 1845 . . 3 wff 𝑥𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)
1413, 5cab 2738 . 2 class {𝑧 ∣ ∃𝑥𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)}
154, 14wceq 1624 1 wff {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {𝑧 ∣ ∃𝑥𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)}
Colors of variables: wff setvar class
This definition is referenced by:  opabss  4858  opabbid  4859  nfopab  4862  nfopab1  4863  nfopab2  4864  cbvopab  4865  cbvopab1  4867  cbvopab2  4868  cbvopab1s  4869  cbvopab2v  4871  unopab  4872  opabid  5124  elopab  5125  ssopab2  5143  iunopab  5154  dfid3  5167  elxpi  5279  rabxp  5303  csbxp  5349  ssrel  5356  relopabi  5393  relopabiALT  5394  opabssxpd  5485  cnv0  5685  dfoprab2  6858  dmoprab  6898  dfopab2  7381  brdom7disj  9537  brdom6disj  9538  opabssi  29724  cnvoprabOLD  29799  cnfinltrel  33544  rnxrn  34471  dropab1  39145  dropab2  39146  csbxpgOLD  39545  csbxpgVD  39621  relopabVD  39628
  Copyright terms: Public domain W3C validator