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 4746
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 5056 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 7266. For example, 𝑅 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ (𝑥 + 1) = 𝑦)} → 3𝑅4 (ex-opab 27419). (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 4745 . 2 class {⟨𝑥, 𝑦⟩ ∣ 𝜑}
5 vz . . . . . . . 8 setvar 𝑧
65cv 1522 . . . . . . 7 class 𝑧
72cv 1522 . . . . . . . 8 class 𝑥
83cv 1522 . . . . . . . 8 class 𝑦
97, 8cop 4216 . . . . . . 7 class 𝑥, 𝑦
106, 9wceq 1523 . . . . . 6 wff 𝑧 = ⟨𝑥, 𝑦
1110, 1wa 383 . . . . 5 wff (𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)
1211, 3wex 1744 . . . 4 wff 𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)
1312, 2wex 1744 . . 3 wff 𝑥𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)
1413, 5cab 2637 . 2 class {𝑧 ∣ ∃𝑥𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)}
154, 14wceq 1523 1 wff {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {𝑧 ∣ ∃𝑥𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)}
Colors of variables: wff setvar class
This definition is referenced by:  opabss  4747  opabbid  4748  nfopab  4751  nfopab1  4752  nfopab2  4753  cbvopab  4754  cbvopab1  4756  cbvopab2  4757  cbvopab1s  4758  cbvopab2v  4760  unopab  4761  opabid  5011  elopab  5012  ssopab2  5030  iunopab  5041  dfid3  5054  elxpi  5164  rabxp  5188  csbxp  5234  ssrel  5241  relopabi  5278  relopabiALT  5279  opabssxpd  5370  cnv0  5570  dfoprab2  6743  dmoprab  6783  dfopab2  7266  brdom7disj  9391  brdom6disj  9392  opabssi  29551  cnvoprabOLD  29626  rnxrn  34296  dropab1  38968  dropab2  38969  csbxpgOLD  39368  csbxpgVD  39444  relopabVD  39451
  Copyright terms: Public domain W3C validator