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 4907
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 5222 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 7450. For example, 𝑅 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ (𝑥 + 1) = 𝑦)} → 3𝑅4 (ex-opab 27616). (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 4906 . 2 class {⟨𝑥, 𝑦⟩ ∣ 𝜑}
5 vz . . . . . . . 8 setvar 𝑧
65cv 1636 . . . . . . 7 class 𝑧
72cv 1636 . . . . . . . 8 class 𝑥
83cv 1636 . . . . . . . 8 class 𝑦
97, 8cop 4376 . . . . . . 7 class 𝑥, 𝑦
106, 9wceq 1637 . . . . . 6 wff 𝑧 = ⟨𝑥, 𝑦
1110, 1wa 384 . . . . 5 wff (𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)
1211, 3wex 1859 . . . 4 wff 𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)
1312, 2wex 1859 . . 3 wff 𝑥𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)
1413, 5cab 2792 . 2 class {𝑧 ∣ ∃𝑥𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)}
154, 14wceq 1637 1 wff {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {𝑧 ∣ ∃𝑥𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)}
Colors of variables: wff setvar class
This definition is referenced by:  opabss  4908  opabbid  4909  nfopab  4912  nfopab1  4913  nfopab2  4914  cbvopab  4915  cbvopab1  4917  cbvopab2  4918  cbvopab1s  4919  cbvopab2v  4921  unopab  4922  opabid  5177  elopab  5178  ssopab2  5196  iunopab  5207  dfid3  5220  elxpi  5332  rabxp  5354  csbxp  5402  ssrel  5409  relopabi  5447  relopabiALT  5448  opabssxpd  5539  cnv0  5746  dfoprab2  6927  dmoprab  6967  dfopab2  7450  brdom7disj  9634  brdom6disj  9635  opabssi  29746  cnvoprabOLD  29821  cnfinltrel  33552  rnxrn  34464  dropab1  39143  dropab2  39144  csbxpgOLD  39542  csbxpgVD  39618  relopabVD  39625
  Copyright terms: Public domain W3C validator