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 4684
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 5002 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 7182. For example, 𝑅 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ (𝑥 + 1) = 𝑦)} → 3𝑅4 (ex-opab 27177). (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 4682 . 2 class {⟨𝑥, 𝑦⟩ ∣ 𝜑}
5 vz . . . . . . . 8 setvar 𝑧
65cv 1479 . . . . . . 7 class 𝑧
72cv 1479 . . . . . . . 8 class 𝑥
83cv 1479 . . . . . . . 8 class 𝑦
97, 8cop 4161 . . . . . . 7 class 𝑥, 𝑦
106, 9wceq 1480 . . . . . 6 wff 𝑧 = ⟨𝑥, 𝑦
1110, 1wa 384 . . . . 5 wff (𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)
1211, 3wex 1701 . . . 4 wff 𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)
1312, 2wex 1701 . . 3 wff 𝑥𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)
1413, 5cab 2607 . 2 class {𝑧 ∣ ∃𝑥𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)}
154, 14wceq 1480 1 wff {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {𝑧 ∣ ∃𝑥𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)}
Colors of variables: wff setvar class
This definition is referenced by:  opabss  4686  opabbid  4687  nfopab  4690  nfopab1  4691  nfopab2  4692  cbvopab  4693  cbvopab1  4695  cbvopab2  4696  cbvopab1s  4697  cbvopab2v  4699  unopab  4700  opabid  4952  elopab  4953  ssopab2  4971  iunopab  4982  dfid3  5000  elxpi  5100  rabxp  5124  csbxp  5171  ssrel  5178  relopabi  5215  relopabiALT  5216  opabssxpd  5308  cnv0  5504  dfoprab2  6666  dmoprab  6706  dfopab2  7182  brdom7disj  9313  brdom6disj  9314  cnvoprab  29382  dropab1  38172  dropab2  38173  csbxpgOLD  38575  csbxpgVD  38652  relopabVD  38659
  Copyright terms: Public domain W3C validator